Theorem: Total Ordering on Field of Quotients is Unique

Let $\struct {K, +, \circ}$ be a field of quotients of an ordered integral domain $\struct {D, +, \circ, \le}$.
Then there is one and only one total ordering $\le'$ on $K$ which is compatible with its ring structure and induces on $D$ its given total ordering $\le$.
That ordering is the one defined by:
:$P = \set {\dfrac x y \in K: x \in D_+, y \in D_+^*}$

Proof:
First, note that from Divided by Positive Element of Field of Quotients:
:$\forall z \in K: \exists x, y \in R: z = \dfrac x y, y \in R_+^*$
Now we show that $P$ satistfies conditions $(1)$ to $(4)$ of Positive Elements of Ordered Ring.
From Addition of Division Products and Product of Division Products, it is clear that $P$ satisfies $(1)$ and $(3)$.
{{qed|lemma}}
Next we establish $(2)$.
Let $z \in P \cap \paren {-P}$.
Then $z \in P$ and $z \in \paren {-P}$. Thus:
:$\exists x_1, x_2 \in D_+, y_1, y_2 \in D_+^*: z = x_1 / y_1, -z = x_2 / y_2$
So:
:$x_1 / y_1 = -\paren {x_2 / y_2} \implies x_1 \circ y_2 = -\paren {x_2 \circ y_1}$
But $0 \le x_1 \circ y_2$ and $-\paren {x_2 \circ y_1} \le 0$.
So $x_1 \circ y_2 = 0$.
As $0 < y_2$, this means $x = 0$ and therefore $z = 0$.
Thus $(2)$ has been established.
{{qed|lemma}}
Now to show that $(4)$ holds.
Let $z = x / y$ where $x \in D, y \in D_+$.
Suppose $0 \le x$. Then $z \in P$.
However, suppose $x < 0$. Then $0 < \paren {-x}$ so $-z = \paren {-x} / y \in P$.
Thus:
:$z = -\paren {-z} \in -P$
So:
:$P \cup \paren {-P} = K$
So by Positive Elements of Ordered Ring, the relation $\le'$ on $K$ defined by $P$ is a total ordering on $K$ compatible with its ring structure.
{{qed|lemma}}
Now we need to show that the ordering induced on $D$ by $\le'$ is indeed $\le$.
Let $z \in D_+$. Then $z = z / 1_D \in P$, as $1_D \in D_+^*$.
Thus $D_+ \subseteq P$ and $D_+ \subseteq D$ so $D_+ \subseteq D \cap P$ from Intersection is Largest Subset.
Conversely, let $z \in D \cap P$. Then:
:$\exists x \in D_+, y \in D_+^*: z = x / y$
If $x = 0$ then $z = 0$, and if $0 < x$ then as $z \circ y = x$ and $0 < y$, it follows that $0 < z$ by item 1 of Properties of a Totally Ordered Ring.
So $\forall z \in D: 0 \le z \iff z \in P$.
Thus it follows that $z \in D \cap P \implies z \in D_+$, i.e. $D \cap P \subseteq D_+$.
Thus $D_+ = D \cap P$.
By item $(2)$ of Properties of Ordered Ring, we have:
:$x \le y \iff 0 \le y + \left({-x}\right)$
and thus it follows that the ordering induced on $D$ by $\le'$ is $\le$.
{{qed|lemma}}
Now we need to show uniqueness.
Let $\preceq$ be a total ordering on $K$ which is compatible with its ring structure and induces on $D$ the ordering $\le$.
Let $Q = \set {z \in K: 0 \preceq z}$.
We now show that $Q = P$.
Let $x \in D_+, y \in D_+^*$.
Then $0 \preceq x$ and $0 \prec 1 / y$ from item 4 of Properties of a Totally Ordered Ring.
Thus by compatibility with ring structure, $0 \preceq x / y$.
Hence $P \subseteq Q$.
Conversely, let $z \in Q$.
Let $z = x / y$ where $x \in D, y \in D_+^*$.
Then $x = z \circ y$ and by compatibility with ring structure, $0 \preceq x$.
Thus $0 \le x$ and hence $z \in P$, and so $Q \subseteq P$.
So $Q = P$.
Therefore, by item $(2)$ of Properties of Ordered Ring, it follows that $\preceq$ is the same as $\le$.
{{Qed}}
{{improve|Put this in the context of Ordered Integral Domain.}}