Well-Founded Relation

DEF-WF. Well-Founded Relation.

A binary relation $\sim$ on $X$ is well-founded if every non-empty subset $A\subseteq X$ has an element $a\in A$ such that

\[\forall x\in A : x\not\sim a.\]