WF#DEF. Well-Founded Relation.
A binary relation $\sim$ on $X$ is well-founded if every non-empty subset $A\subseteq X$ has a $\sim$-minimal element, i.e. an element $a\in A$ such that
\[\forall x\in A : x\not\sim a.\]
WF#DEF. Well-Founded Relation.
A binary relation $\sim$ on $X$ is well-founded if every non-empty subset $A\subseteq X$ has a $\sim$-minimal element, i.e. an element $a\in A$ such that
\[\forall x\in A : x\not\sim a.\]