Axiom. radd_assoc
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → (a + b) + c = a + (b + c)