Theorem rsub_neg

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. ⊢ a - b = a + -b, rsub_eq.
04. ⊢ -(a - b) = -(a + -b), eq_cong 3, f t = -t.
05. 2 ⊢ -b ∈ ℝ, rneg_closed 2.
06. 1, 2 ⊢ -(a + -b) = -a + -(-b), rneg_dist_add 1 5.
07. 1, 2 ⊢ -(a - b) = -a + -(-b), eq_trans 4 6.
08. 2 ⊢ -(-b) = b, rneg_involution 2.
09. 1, 2 ⊢ -(a - b) = -a + b,
  eq_subst 8 7, P t ↔ -(a - b) = -a + t.
10. 1 ⊢ -a ∈ ℝ, rneg_closed 1.
11. 1, 2 ⊢ -a + b = b + -a, radd_comm 10 2.
12. ⊢ b - a = b + -a, rsub_eq.
13. 1, 2 ⊢ -a + b = b - a, eq_trans_rr 11 12.
14. 1, 2 ⊢ -(a - b) = b - a, eq_trans 9 13.
rsub_neg. ⊢ a ∈ ℝ → b ∈ ℝ → -(a - b) = b - a,
  subj_intro_ii 14.

Dependencies
The given proof depends on 12 axioms:
eq_refl, eq_subst, radd_assoc, radd_closed, radd_comm, radd_inv, radd_neutr, rmul_closed, rmul_comm, rmul_distl_add, rmul_neutr, rneg_closed.