Axiom. rle_trans
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a ≤ b → b ≤ c → a ≤ c