Axiom. rle_total
a ∈ ℝ → b ∈ ℝ → a ≤ b ∨ b ≤ a