Definition:Foundational Relation

Definition

Let $\left({A, \prec}\right)$ be a relational structure and let $A$ be either a proper class or a set.

Then $\prec$ is a Foundational Relation on $A$ iff every nonempty subset of $A$ has a least element.

That is, expressed symbolically, $\prec$ is a foundational relation on $A$ iff

$\forall x: \left({x \subseteq A \land x \ne \varnothing}\right) \implies \exists y \in x: \forall z \in x: \neg z \prec y$

where $\varnothing$ is the empty set.