Closed Interval of Naturally Ordered Semigroup with Successor equals Union with Successor

Theorem

Let $\left({S, \circ, \preceq}\right)$ be a naturally ordered semigroup.

Then:

$\forall m, n \in \left({S, \circ, \preceq}\right): m \preceq n \implies \left[{m \,.\,.\, n \circ 1}\right] = \left[{m \,.\,.\, n}\right] \cup \left\{{n \circ 1}\right\}$

where $\left[{m \,.\,.\, n}\right]$ is the closed interval between $m$ and $n$.

Proof

Let $m \preceq n$. Then:

 $\ds$  $\ds x \in \left[{m \,.\,.\, n \circ 1}\right]$ $\ds$ $\iff$ $\ds m \preceq x \land x \preceq \left({n \circ 1}\right)$ Definition of Closed Interval $\ds$ $\iff$ $\ds m \preceq x \land \left({x \prec n \circ 1 \lor x = n \circ 1}\right)$ Definition of Strictly Precedes

 $\ds$  $\ds x \in \left[{m \,.\,.\, n}\right] \cup \left\{ {n \circ 1}\right\}$ $\ds$ $\iff$ $\ds m \preceq x \land \left({x \preceq n \lor x = n \circ 1}\right)$ Definitions of Closed Interval and Union $\ds$ $\iff$ $\ds m \preceq x \land \left({x \prec n \lor x = n \lor x = n \circ 1}\right)$ Definition of Strictly Precedes $\ds$ $\iff$ $\ds m \preceq x \land \left({x \prec n \circ 1 \lor x = n \circ 1}\right)$ Definition of Strictly Precedes

Thus:

$\left[{m \,.\,.\, n \circ 1}\right] = \left[{m \,.\,.\, n}\right] \cup \left\{{n \circ 1}\right\}$

$\blacksquare$