Set is Subset of Finite Infima Set

Theorem

Let $\left({S, \preceq}\right)$ be an ordered set.

Let $X$ be a subset of $S$.

Then $X \subseteq \operatorname{fininfs}\left({X}\right)$

where $\operatorname{fininfs}\left({X}\right)$ denotes the finite infima set of $X$.

Proof

Let $x \in X$.

By Infimum of Singleton:

$\left\{ {x}\right\}$ admits an infimum and $\inf \left\{ {x}\right\} = x$

By definitions of subset and singleton:

$\left\{ {x}\right\} \subseteq X$

By Singleton is Finite:

$\left\{ {x}\right\}$ is a finite set.

Thus by definition of finite infima set:

$x \in \operatorname{fininfs}\left({X}\right)$

$\blacksquare$

Sources

• Mizar article WAYBEL_0:50