Square of Element Less than Unity in Ordered Integral Domain

Theorem

Let $\struct {D, +, \times, \le}$ be an ordered integral domain.

Let $x \in D$ such that $0 < x < 1$.

Then:

$0 < x \times x < x$

Proof

We have that $0 < x < 1$.

From Relation Induced by Strict Positivity Property is Compatible with Multiplication:

$0 \times x < x \times x < 1 \times x$

Hence the result.

$\blacksquare$