Axiom. rinv_closed
a ∈ ℝ → ¬a = 0 → /a ∈ ℝ