Well-founded relation
In mathematics, a binary relation R is called well-founded (or wellfounded or foundational) on a set or, more generally, a class X if every non-empty subset (or subclass) S ⊆ X has a minimal element with respect to R; that is, there exists an m ∈ S such that for every s ∈ S, one does not have s R m. More formally, a relation is well-founded if: ( ∀ S ⊆ X ) [ S ≠ ∅ ⟹ ( ∃ m ∈ S ) ( ∀ s ∈ S ) ¬ ( s R m ) ] .