Theorem: Subsets Greater Than and Less Than Identity of Ordered Abelian Group are Isomorphic Ordered Semigroups

Let $\struct {G, \circ, \preccurlyeq}$ be an ordered abelian group whose identity element is $e$.
Let $G^+$ and $G^-$ denote the subsets of $G$ defined as:
:$G^+ = \set {x \in G: e \preccurlyeq x}$
:$G^- = \set {x \in G: x \preccurlyeq e}$
Then $\struct {G^+, \circ, \preccurlyeq}$ and $\struct {G^-, \circ, \succcurlyeq}$ are subsemigroups of $G$ such that the inversion mapping $\iota: G \to G$ defined as:
:$\forall g \in G: \map \iota g = g^{-1}$
is:
:an isomorphism from $\struct {G^+, \circ, \preccurlyeq}$ to $\struct {G^-, \circ, \succcurlyeq}$
and:
:an isomorphism from $\struct {G^-, \circ, \preccurlyeq}$ to $\struct {G^+, \circ, \succcurlyeq}$

Proof:
Let $x, y \in G^+$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = e
      | o = \preccurlyeq
      | r = x
      | c = Definition of $G^+$
}}
{{eqn | l = e
      | o = \preccurlyeq
      | r = y
      | c = Definition of $G^+$
}}
{{eqn | ll= \leadsto
      | l = e \circ y
      | o = \preccurlyeq
      | r = x \circ y
      | c = {{Defof|Ordered Group}} as $\preccurlyeq$ is compatible with $\circ$
}}
{{eqn | l = x \circ e
      | o = \preccurlyeq
      | r = x \circ y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e
      | o = \preccurlyeq
      | r = x \circ y
      | c = $\preccurlyeq$ is an ordering and therefore transitive
}}
{{eqn | ll= \leadsto
      | l = x \circ y
      | o = \in
      | r = G^+
      | c = Definition of $G^+$
}}
{{end-eqn}}
So by the Subsemigroup Closure Test $\struct {G^+, \circ}$ is a subsemigroup of $\struct {G, \circ}$.
{{qed|lemma}}
Let $x, y \in G^-$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | l = x
      | o = \preccurlyeq
      | r = e
      | c = Definition of $G^-$
}}
{{eqn | l = y
      | o = \preccurlyeq
      | r = e
      | c = Definition of $G^-$
}}
{{eqn | ll= \leadsto
      | l = x \circ y
      | o = \preccurlyeq
      | r = x \circ e
      | c = {{Defof|Ordered Group}} as $\preccurlyeq$ is compatible with $\circ$
}}
{{eqn | l = x \circ y
      | o = \preccurlyeq
      | r = e \circ y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \circ y
      | o = \preccurlyeq
      | r = e
      | c = $\preccurlyeq$ is an ordering and therefore transitive
}}
{{eqn | ll= \leadsto
      | l = x \circ y
      | o = \in
      | r = G^-
      | c = Definition of $G^-$
}}
{{end-eqn}}
So by the Subsemigroup Closure Test $\struct {G^-, \circ}$ is a subsemigroup of $\struct {G, \circ}$.
{{qed|lemma}}
Then we establish that:
{{begin-eqn}}
{{eqn | q = \forall x, y \in G
      | l = \map \iota {x \circ y}
      | r = \paren {x \circ y}^{-1}
      | c = {{Defof|Inversion Mapping}}
}}
{{eqn | r = y^{-1} \circ x^{-1}
      | c = Inverse of Group Product
}}
{{eqn | r = x^{-1} \circ y^{-1}
      | c = {{Defof|Abelian Group}}
}}
{{eqn | r = \map \iota x \circ \map \iota y
      | c = {{Defof|Inversion Mapping}}
}}
{{end-eqn}}
demonstrating that for all $\iota$ has the morphism property over the whole of $G$.
Then we note that:
{{begin-eqn}}
{{eqn | q = \forall x \in G^+
      | l = e
      | o = \preccurlyeq
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e
      | o = \succcurlyeq
      | r = x^{-1}
      | c = Inversion Mapping Reverses Ordering in Ordered Group: Corollary
}}
{{eqn | ll= \leadsto
      | l = e
      | o = \succcurlyeq
      | r = \map \iota x
      | c = {{Defof|Inversion Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \map \iota x
      | o = \in
      | r = G^-
      | c = Definition of $G^-$
}}
{{eqn | ll= \leadsto
      | l = \iota \sqbrk {G^+}
      | r = G^-
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{end-eqn}}
Similarly:
{{begin-eqn}}
{{eqn | q = \forall x \in G^-
      | l = e
      | o = \succcurlyeq
      | r = x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = e
      | o = \preccurlyeq
      | r = x^{-1}
      | c = Inversion Mapping Reverses Ordering in Ordered Group: Corollary
}}
{{eqn | ll= \leadsto
      | l = e
      | o = \preccurlyeq
      | r = \map \iota x
      | c = {{Defof|Inversion Mapping}}
}}
{{eqn | ll= \leadsto
      | l = \map \iota x
      | o = \in
      | r = G^+
      | c = Definition of $G^+$
}}
{{eqn | ll= \leadsto
      | l = \iota \sqbrk {G^-}
      | r = G^+
      | c = {{Defof|Image of Subset under Mapping}}
}}
{{end-eqn}}
Then we note that:
{{begin-eqn}}
{{eqn | q = \forall x, y \in G
      | l = \map \iota x
      | r = \map \iota y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x^{-1}
      | r = y^{-1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = y
      | c = {{Group-axiom|3}}
}}
{{end-eqn}}
demonstrating that $\iota$ is an injection.
Let $x \in G^+$.
Then {{apriori}}:
:$\exists x^{-1} \in G^-: \map \iota {x^{-1} } = x$
Similarly, let $x \in G^-$.
Then {{apriori}}:
:$\exists x^{-1} \in G^+: \map \iota {x^{-1} } = x$
So $\iota: G^+ \to G^-$ and $\iota: G^- \to G^+$ are both surjections.
Hence $\iota: G^+ \to G^-$ and $\iota: G^- \to G^+$ are both bijections by definition.
Thus we have that:
:$\iota: \struct {G^+, \circ} \to \struct {G^-, \circ}$ is a semigroup isomorphism
and
:$\iota: \struct {G^-, \circ} \to \struct {G^+, \circ}$ is a semigroup isomorphism.
{{qed|lemma}}
Let $x, y \in G^+$ be arbitrary, such that $x \preccurlyeq y$.
We have:
{{begin-eqn}}
{{eqn | l = x
      | o = \preccurlyeq
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x^{-1}
      | o = \succcurlyeq
      | r = y^{-1}
      | c = Inversion Mapping Reverses Ordering in Ordered Group
}}
{{eqn | ll= \leadsto
      | l = \map \iota x
      | o = \succcurlyeq
      | r = \map \iota y
      | c = {{Defof|Inversion Mapping}}
}}
{{end-eqn}}
Let $x, y \in G^-$ be arbitrary, such that $x \succcurlyeq y$.
We have:
{{begin-eqn}}
{{eqn | l = x
      | o = \succcurlyeq
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x^{-1}
      | o = \preccurlyeq
      | r = y^{-1}
      | c = Inversion Mapping Reverses Ordering in Ordered Group
}}
{{eqn | ll= \leadsto
      | l = \map \iota x
      | o = \preccurlyeq
      | r = \map \iota y
      | c = {{Defof|Inversion Mapping}}
}}
{{end-eqn}}
Thus we have demonstrated that $\iota: \struct {G^+, \preccurlyeq} \to \struct {G^-, \succcurlyeq}$ and $\iota: \struct {G^-, \succcurlyeq} \to \struct {G^+, \preccurlyeq}$ are order isomorphisms.
So we have that:
Thus we have that:
:$\iota: \struct {G^+, \circ} \to \struct {G^-, \circ}$ is a semigroup isomorphism
:$\iota: \struct {G^+, \preccurlyeq} \to \struct {G^-, \succcurlyeq}$ is an order isomorphism
and so:
:$\iota: \struct {G^+, \circ, \preccurlyeq} \to \struct {G^-, \circ, \succcurlyeq}$ is an ordered semigroup isomorphism
and
:$\iota: \struct {G^-, \circ} \to \struct {G^+, \circ}$ is a semigroup isomorphism
:$\iota: \struct {G^-, \succcurlyeq} \to \struct {G^+, \preccurlyeq}$ is an order isomorphism
and so:
:$\iota: \struct {G^-, \circ, \succcurlyeq} \to \struct {G^+, \circ, \preccurlyeq}$ is an ordered semigroup isomorphism
{{qed}}