EDB — 1ZX

[1ZX] In an ordered field \(F\) we call \(P = \{ x ∈ F : x ≥ 0\} \) the set of positive (or zero) numbers; it satisfies the following properties: ¹

• \(x, y ∈ P ⇒ x + y , x · y ∈ P \),

• \(P ∩ (−P ) = \{ 0 \} \) and

• \(P ∪ (−P ) = F \).

vice versa if in a field \(F\) we can find a set \(P⊆ F\) that satisfies them, then \(F\) is an ordered field by defining \(x ≤ y ⇔ y−x ∈ P\).