Axiom. rneg_closed
a ∈ ℝ → -a ∈ ℝ