Strict Ordering can be Expanded to Compare Additional Pair/Proof 1

== Theorem ==
== Proof ==
First, note that since $\prec$ is a strict ordering, $\preceq$ is an ordering by Reflexive Closure of Strict Ordering is Ordering.
=== $a$ and $b$ are $\preceq$-incomparable ===
Suppose that $a \preceq b$.
By the definition of reflexive closure, either $a \prec b$ or $a = b$.
Each possibility contradicts one of the premises, so $a \npreceq b$.
For the same reasons, $b \npreceq a$.
=== $\prec'^+$ is antireflexive ===
Let $p \in S$.
Then by the definition of strict ordering:
$p \nprec p$.
Suppose that $p \preceq a$ and $b \preceq p$.
Then since $\preceq$ is transitive, $b \preceq a$, contradicting the fact that $a$ and $b$ are $\preceq$-incomparable.
Since neither $p \prec p$ nor $\paren {p \preceq a} \land \paren {b \preceq p}$ holds:
:$p \nprec'^+ p$.
Since this is the case for all $p \in S$, $\prec'^+$ is antireflexive.
=== $\prec'^+$ is transitive ===
Let $p \prec'^+ q$ and $q \prec'^+ r$.
Then there are three possibilities:
$(1): \quad p \prec q$ and $p \prec r$
Because $\prec$ is transitive:
:$p \prec r$
Thus:
:$p \prec'^+ r$
$(2): \quad p \prec q$, $q \preceq a$, and $b \preceq r$
By Extended Transitivity, $p \prec a$.
Since $p \prec a$ and $b \prec r$:
:$p \prec'^+ r$
$(3): \quad p \preceq a$, $b \preceq q$, and $q \prec r$
By Extended Transitivity:
:$b \prec r$
Therefore:
:$b \preceq r$
Since $p \preceq a$ and $b \preceq r$:
:$p \prec'^+ r$
Note that it is impossible to have $p \preceq a$, $b \preceq q$, $q \preceq a$ and $b \preceq r$.
If that were so, $b \preceq q$ and $q \preceq a$ together would imply by transitivity that $b \preceq a$.
But this contradicts the fact that $a$ and $b$ are $\preceq$-incomparable.
Thus in all cases, $p \prec'^+ q$ and $q \prec'^+ r$ imply $p \prec'^+ r$, so $\prec'^+$ is transitive.
Since $\prec'^+$ is transitive and antireflexive, it is by definition a strict ordering.
=== $\prec'^+$ is the transitive closure of $\prec'$ ===
First note that $\prec'$ is a subset of $\prec'^+$:
If $p \prec' q$ then either
:$p \prec q$ or
:$p = a$ and $q = b$
If $p \prec q$ then $p \prec'^+ q$ by definition.
If $p = a$ and $q = b$, then $p \preceq a$ and $q \preceq b$ by the definition of $\preceq$.
Thus $p \prec'^+ q$ by the definition of $\preceq'^+$.
Let $\RR$ be a transitive relation containing $\prec'$.
Let $p, q \in S$ and let $p \prec'^+ q$.
Then either:
:$p \prec q$ or
:$p \preceq a$ and $b \preceq q$
If $p \prec q$, then by the definition of subset, $p \mathrel \RR q$.
Suppose instead that $p \preceq a$ and $b \preceq q$. By the definition of $\preceq'$, $a \preceq' b$.
Since Reflexive Closure is Closure Operator, it is increasing, so ${\preceq} \subseteq {\RR^=}$.
Thus $p \mathrel {\RR^=} a$, $a \mathrel {\RR^=} b$, and $b \mathrel {\RR^=} q$.
Since $\RR$ is transitive, $\RR^=$ is as well, by Reflexive Closure of Transitive Relation is Transitive.
Thus $p \mathrel {\RR^=} q$.
Since $\preceq'^+$ is antireflexive and we assumed $p \preceq'^+ q$, we conclude that $p \ne q$.
Thus by the definition of reflexive closure:
:$p \mathrel \RR q$
Thus we have shown that $\preceq'^+$ is a subset of $\RR$.
Since this holds when $\RR$ is any transitive superset of $\preceq'$, $\preceq'^+$ is the transitive closure of $\preceq'$.
Category:Strict Ordering can be Expanded to Compare Additional Pair