Theorem rsub_from_zero

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 1 ⊢ -a ∈ ℝ, rneg_closed 1.
03. ⊢ 0 - a = 0 + (-a), rsub_eq.
04. 1 ⊢ 0 + (-a) = -a, radd_neutl 2.
05. 1 ⊢ 0 - a = -a, eq_trans 3 4.
rsub_from_zero. ⊢ a ∈ ℝ → 0 - a = -a, subj_intro 5.

Dependencies
The given proof depends on five axioms:
eq_refl, eq_subst, radd_comm, radd_neutr, rneg_closed.