Theorem: Strict Ordering on Integers is Trichotomy

Let $\eqclass {a, b} {}$ and $\eqclass {c, d} {}$ be integers, as defined by the formal definition of integers.
Then exactly one of the following holds:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | l = \eqclass {a, b} {}
      | o = =
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | l = \eqclass {a, b} {}
      | o = >
      | r = \eqclass {c, d} {}
      | c = 
}}
{{end-eqn}}
That is, strict ordering is a trichotomy.

Proof:
By the formal definition of integers, we have that $a, b, c, d, e, f$ are all natural numbers.
To eliminate confusion between integer ordering and the ordering on the natural numbers, let $a \preccurlyeq b$ denote that the natural number $a$ is less than or equal to the natural number $b$.
We have:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass {c, d} {}
      | o = \nless
      | r = \eqclass {a, b} {}
      | c = Strict Ordering on Integers is Asymmetric
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = \prec
      | r = b + c
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = \ne
      | r = b + c
      | c = {{Defof|Ordering on Natural Numbers}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a, b} {}
      | o = \ne
      | r = \eqclass {c, d} {}
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = >
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \eqclass {c, d} {}
      | o = \ngtr
      | r = \eqclass {a, b} {}
      | c = Strict Ordering on Integers is Asymmetric
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = >
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = \succ
      | r = b + c
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = \ne
      | r = b + c
      | c = {{Defof|Ordering on Natural Numbers}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a, b} {}
      | o = \ne
      | r = \eqclass {c, d} {}
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = =
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = =
      | r = b + c
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = \nprec
      | r = b + c
      | c = {{Defof|Ordering on Natural Numbers}}
}}
{{eqn | lo= \land
      | l = a + d
      | o = \nsucc
      | r = b + c
      | c = {{Defof|Ordering on Natural Numbers}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a, b} {}
      | o = \nless
      | r = \eqclass {c, d} {}
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | lo= \land
      | l = \eqclass {a, b} {}
      | o = \ngtr
      | r = \eqclass {c, d} {}
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{end-eqn}}
This demonstrates that $<$, $=$ and $>$ are mutually exclusive.
Now:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = \prec
      | r = b + c
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | ll= \leadsto
      | l = b + c
      | o = \preccurlyeq
      | r = a + d
      | c = {{Defof|Ordering on Natural Numbers}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass {c, d} {}
      | o = \le
      | r = \eqclass {a, b} {}
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = >
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = \succ
      | r = b + c
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | ll= \leadsto
      | l = b + c
      | o = \succcurlyeq
      | r = a + d
      | c = {{Defof|Ordering on Natural Numbers}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass {c, d} {}
      | o = \ge
      | r = \eqclass {a, b} {}
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \eqclass {a, b} {}
      | o = \ne
      | r = \eqclass {c, d} {}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = \ne
      | r = b + c
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | ll= \leadsto
      | l = a + d
      | o = \prec
      | r = b + c
      | c = {{Defof|Ordering on Natural Numbers}}
}}
{{eqn | lo= \lor
      | l = a + d
      | o = \succ
      | r = b + c
      | c = {{Defof|Ordering on Natural Numbers}}
}}
{{eqn | ll= \leadsto
      | l = \eqclass {a, b} {}
      | o = <
      | r = \eqclass {c, d} {}
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{eqn | lo= \land
      | l = \eqclass {a, b} {}
      | o = \>
      | r = \eqclass {c, d} {}
      | c = {{Defof|Strict Ordering on Integers}}
}}
{{end-eqn}}
demonstrating that either $<$, $=$ or $>$ must hold.
{{qed}}