Singleton is Chain
Jump to navigation
Jump to search
Theorem
Let $\struct {S, \preceq}$ be an ordered set.
Let $x \in S$.
Then $\set x$ is a chain of $\struct {S, \preceq}$.
Proof
It suffices to prove that
- $\set x$ is connected
Let $y, z \in \set x$.
By definition of singleton:
- $y = x$ and $z = x$
By definition of reflexivity;
- $y \preceq z$
Thus
- $y \preceq z$ or $z \preceq y$
$\blacksquare$
Sources
- Mizar article ORDERS_2:8