Axiom. radd_closed
a ∈ ℝ → b ∈ ℝ → a + b ∈ ℝ