Axiom. rmul_closed
a ∈ ℝ → b ∈ ℝ → a⋅b ∈ ℝ