Theorem rsub_closed

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 2 ⊢ -b ∈ ℝ, rneg_closed 2.
04. 1, 2 ⊢ a + -b ∈ ℝ, radd_closed 1 3.
05. 1, 2 ⊢ a - b ∈ ℝ,
  eq_subst_rev rsub_eq 4, P t ↔ t ∈ ℝ.
rsub_closed. ⊢ a ∈ ℝ → b ∈ ℝ → a - b ∈ ℝ,
  subj_intro_ii 5.

Dependencies
The given proof depends on four axioms:
eq_refl, eq_subst, radd_closed, rneg_closed.