Characterization of Minimal Element
If you are fairly certain that there are none, please remove {{proofread}} from the code.
In particular: including category.
You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links.
To discuss this in more detail, feel free to use the talk page.
Once you have done so, you can remove this instance of {{MissingLinks}} from the code.
Theorem
Let $C$ be a class.
Let $\prec$ be a relation on $C$.
Let $B$ be a subclass of $C$.
Let $x \in B$.
Let $S_x = \left\{ {y \in C: y \prec x \text{ and } y \ne x}\right\}$ be the initial segment of $x$ in $C$.
Then $x$ is a minimal element of $B$ if and only if $B \cap S_x = \varnothing$.
Proof
Necessary Condition
Suppose $x$ is a minimal element of $B$.
Then for each $z \in B$ such that $z \ne x$, $z \not \prec x$.
Thus $S_x \cap B = \varnothing$.
$\Box$
Sufficient Condition
Suppose that $x$ is not a minimal element of $B$.
Then for some $z \in B$, $z \prec x$ and $z \ne x$.
Thus $z \in S_x$.
Since $z \in B$, $B \cap S_x \ne \varnothing$.
$\blacksquare$
