Bottom in Ideal

Theorem

Let $\struct {S, \preceq}$ be a bounded below ordered set.

Let $I$ be a ideal in $S$.

Then $\bot \in I$

where $\bot$ denotes the smallest element of $S$.

Proof

By definition of ideal in ordered set:

$I$ is non-empty and lower.

By definition of non-empty set:

$\exists x: x \in I$

By definition of smallest element:

$\bot \preceq x$

Thus by definition of lower section:

$\bot \in I$

$\blacksquare$

Sources

• Mizar article WAYBEL_4:21