Theorem rabs_non_positive

Proof
01. 1 ⊢ x ∈ ℝ, hypo.
02. 2 ⊢ x ≤ 0, hypo.
03. ⊢ 0 ∈ ℝ, calc.
04. ⊢ 0 ≤ x ∨ ¬0 ≤ x, lem.
05. 5 ⊢ 0 ≤ x, hypo.
06. 1, 2, 5 ⊢ x = 0, rle_antisym 1 3 2 5.
07. ⊢ 0 ≤ 0, rle_refl 3.
08. ⊢ abs 0 = 0, rabs_eql 3 7.
09. ⊢ -0 = 0, calc.
10. 1, 2, 5 ⊢ -x = -0, eq_cong 6, f t = -t.
11. 1, 2, 5 ⊢ -x = 0, eq_trans 10 9.
12. 1, 2, 5 ⊢ abs x = 0, eq_subst_rev 6 8, P t ↔ abs t = 0.
13. 1, 2, 5 ⊢ abs x = -x, eq_trans_rr 12 11.
14. 14 ⊢ ¬0 ≤ x, hypo.
15. 1, 14 ⊢ abs x = -x, rabs_eqr 1 14.
16. 1, 2 ⊢ abs x = -x, disj_elim 4 13 15.
rabs_non_positive. ⊢ x ∈ ℝ → x ≤ 0 → abs x = -x,
  subj_intro_ii 16.

Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, rle_antisym, rle_refl, rneg_closed.