Set is Subset of Finite Suprema Set
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \preceq}$ be an ordered set.
Let $X$ be a subset of $S$.
Then $X \subseteq \map {\mathrm {finsups} } X$
where $\map {\mathrm {finsups} } X$ denotes finite suprema set of $X$.
Proof
Let $x \in X$.
- $\set x$ admits a supremum and $\sup \set x = x$
By definitions of subset and singleton:
- $\set x \subseteq X$
- $\set x$ is a finite set.
Thus by definition of finite suprema set:
- $x \in \map {\mathrm {finsups} } X$
$\blacksquare$
Sources
- Mizar article WAYBEL_0:50