\begin{definition}[Definition:Ordered Integral Domain/Definition 2]
An '''ordered integral domain''' is an ordered ring $\struct {D, +, \times, \le}$ which is also an integral domain.
That is, it is an integral domain with an ordering $\le$ compatible with the ring structure of $\struct {D, +, \times}$:
{{begin-axiom}}
{{axiom | n = \text {OID} 1
        | lc= $\le$ is compatible with ring addition:
        | q = \forall a, b, c \in D
        | ml= a \le b
        | mo= \implies
        | mr= \paren {a + c} \le \paren {b + c}
}}
{{axiom | n = \text {OID} 2
        | lc= Strict positivity is closed under ring product:
        | q = \forall a, b \in D
        | ml= 0_D \le a, 0_D \le b
        | mo= \implies
        | mr= 0_D \le a \times b
}}
{{end-axiom}}
where $0_D$ is the zero of $D$.
\end{definition}