Axiom. rle_antisym
a ∈ ℝ → b ∈ ℝ → a ≤ b → b ≤ a → a = b