Set is Subset of Upper Closure
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 X^\succeq$
where $X^\succeq$ denotes the upper closure of $X$.
Proof
Let $x \in X$.
By definition of reflexivity:
- $x \preceq x$
Thus by definition of upper closure:
- $x \in X^\succeq$
$\blacksquare$
Sources
- Mizar article WAYBEL_0:16