Upper Closure is Strict Upper Closure of Immediate Predecessor

Theorem

Let $\struct {S, \preccurlyeq}$ be a totally ordered set.

Let $b$ be the immediate successor element of $a$:

Then:

$a^\succ = b^\succcurlyeq$

where:

$a^\succ$ is the strict upper closure of $a$

$b^\succcurlyeq$ is the upper closure of $b$.

Proof

Let:

$x \in a^\succ$

By the definition of strict upper closure:

$a \prec x$

By the definition of total ordering:

$x \prec b$ or $x \succcurlyeq b$

If $x \prec b$ then $a \prec x \prec b$, contradicting the premise.

Thus:

$x \succcurlyeq b$

and so:

$x \in b^\succcurlyeq$

By definition of subset:

$a^\succ \subseteq b^\succcurlyeq$

Let:

$x \in b^\succcurlyeq$

By the definition of upper closure:

$b \preccurlyeq x$

Since $a \prec b$, Extended Transitivity shows that $a \prec x$.

Thus:

$x \in a^\succ$

By definition of subset:

$b^\succcurlyeq \subseteq a^\succ$

Therefore by definition of set equality:

$a^\succ = b^\succcurlyeq$

$\blacksquare$