Theorem: Lexicographically Ordered Pair of Ordered Semigroups with Cancellable Elements

Let $\struct {S_1, \circ_1, \preccurlyeq_1}$ and $\struct {S_2, \circ_2, \preccurlyeq_2}$ be ordered semigroups.
Let $\struct {S_1 \times S_2, \odot} := \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}$ denote the '''external direct product''' of $\struct {S_1, \circ_1}$ and $\struct {S_2, \circ_2}$.
Let $\struct {S_1 \times S_2, \preccurlyeq_l} := \struct {S_1, \preccurlyeq_1} \otimes^l \struct {S_2, \preccurlyeq_2}$ denote the '''lexicographic order''' of $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$:
:$\tuple {x_1, x_2} \preccurlyeq_l \tuple {y_1, y_2} \iff \paren {x_1 \prec_1 y_1} \lor \paren {x_1 = y_1 \land x_2 \preccurlyeq_2 y_2}$
Let every element of $\struct {S_1, \circ_1}$ be cancellable.
Then $\struct {S_1 \times S_2, \odot, \preccurlyeq_l}$ is also an ordered semigroup.

Proof:
From Lexicographic Order is Ordering we have that $\struct {S_1 \times S_2, \preccurlyeq_l}$ is an ordered set.
From External Direct Product of Semigroups, $\struct {S_1 \times S_2, \odot}$ is a semigroup.
It remains to be shown that $\preccurlyeq_l$ is compatible with $\odot$.
Let $\tuple {x_1, x_2}, \tuple {y_1, y_2} \in S_1 \times S_2$ be arbitrary such that $\tuple {x_1, x_2} \preccurlyeq_l \tuple {y_1, y_2}$.
;Case $1$: First suppose $x_1 = y_1$.
{{begin-eqn}}
{{eqn | l = \tuple {x_1, x_2}
      | o = \preccurlyeq_l
      | r = \tuple {y_1, y_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1
      | r = y_1
      | c = 
}}
{{eqn | lo= \land
      | l = x_2
      | o = \preccurlyeq_2
      | r = y_2
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall \tuple {z_1, z_2} \in S_1 \times S_2
      | l = x_1 \circ_1 z_1
      | r = y_1 \circ_1 z_1
      | c = {{Defof|Relation Compatible with Operation}}
}}
{{eqn | lo= \land
      | l = x_2 \circ_2 z_2
      | o = \preccurlyeq_2
      | r = y_2 \circ_2 z_2
      | c = 
}}
{{eqn | lo= \land
      | l = z_1 \circ_1 x_1
      | r = z_1 \circ_1 y_1
      | c = 
}}
{{eqn | lo= \land
      | l = z_2 \circ_2 x_2
      | o = \preccurlyeq_2
      | r = z_2 \circ_2 y_2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {x_1 \circ_1 z_1, x_2 \circ_2 z_2}
      | o = \preccurlyeq_l
      | r = \tuple {y_1 \circ_1 z_1, y_2 \circ_2 z_2}
      | c = {{Defof|Lexicographic Order}}
}}
{{eqn | lo= \land
      | l = \tuple {z_1 \circ_1 x_1, z_2 \circ_2 x_2}
      | o = \preccurlyeq_l
      | r = \tuple {z_1 \circ_1 y_1, z_2 \circ_2 y_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {x_1, x_2} \odot \tuple {z_1, z_2}
      | o = \preccurlyeq_l
      | r = \tuple {y_1, y_2} \odot \tuple {z_1, z_2}
      | c = {{Defof|External Direct Product}}
}}
{{eqn | lo= \land
      | l = \tuple {z_1, z_2} \odot \tuple {x_1, x_2}
      | o = \preccurlyeq_l
      | r = \tuple {z_1, z_2} \odot \tuple {y_1, y_2}
      | c = 
}}
{{end-eqn}}
;Case $2$: Now suppose $x_1 \prec_1 y_1$.
{{begin-eqn}}
{{eqn | l = \tuple {x_1, x_2}
      | o = \preccurlyeq_l
      | r = \tuple {y_1, y_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x_1
      | o = \prec_1
      | r = y_1
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \forall \tuple {z_1, z_2} \in S_1 \times S_2
      | l = x_1 \circ_1 z_1
      | o = \prec_1
      | r = y_1 \circ_1 z_1
      | c = Reflexive Reduction of Relation Compatible with Cancellable Operation is Compatible
}}
{{eqn | lo= \land
      | l = z_1 \circ_1 x_1
      | o = \prec_1
      | r = z_1 \circ_1 y_1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {x_1 \circ_1 z_1, x_2 \circ_2 z_2}
      | o = \preccurlyeq_l
      | r = \tuple {y_1 \circ_1 z_1, y_2 \circ_2 z_2}
      | c = {{Defof|Lexicographic Order}}
}}
{{eqn | lo= \land
      | l = \tuple {z_1 \circ_1 x_1, z_2 \circ_2 x_2}
      | o = \preccurlyeq_l
      | r = \tuple {z_1 \circ_1 y_1, z_2 \circ_2 y_2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tuple {x_1, x_2} \odot \tuple {z_1, z_2}
      | o = \preccurlyeq_l
      | r = \tuple {y_1, y_2} \odot \tuple {z_1, z_2}
      | c = {{Defof|External Direct Product}}
}}
{{eqn | lo= \land
      | l = \tuple {z_1, z_2} \odot \tuple {x_1, x_2}
      | o = \preccurlyeq_l
      | r = \tuple {z_1, z_2} \odot \tuple {y_1, y_2}
      | c = 
}}
{{end-eqn}}
and the proof is complete.
{{qed}}