Theorem rle_lt_tricho

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. ⊢ b < a ∨ ¬b < a, lem.
04. 4 ⊢ b < a, hypo.
05. 4 ⊢ a ≤ b ∨ b < a, disj_intror 4.
06. 6 ⊢ ¬b < a, hypo.
07. ⊢ b < a ↔ b ≤ a ∧ ¬b = a, lt_equi.
08. 6 ⊢ ¬(b ≤ a ∧ ¬b = a), rsubj_tollens 7 6.
09. 6 ⊢ ¬b ≤ a ∨ ¬¬b = a, neg_conj 8.
10. 10 ⊢ ¬b ≤ a, hypo.
11. 1, 2, 10 ⊢ a ≤ b, rle_neg 2 1 10.
12. 1, 2, 10 ⊢ a ≤ b ∨ b < a, disj_introl 11.
13. 13 ⊢ ¬¬b = a, hypo.
14. 13 ⊢ b = a, dne 13.
15. 13 ⊢ a = b, eq_symm 14.
16. 1 ⊢ a ≤ a, rle_refl 1.
17. 1, 13 ⊢ a ≤ b, le_eq_trans 16 15.
18. 1, 13 ⊢ a ≤ b ∨ b < a, disj_introl 17.
19. 1, 2, 6 ⊢ a ≤ b ∨ b < a, disj_elim 9 12 18.
20. 1, 2 ⊢ a ≤ b ∨ b < a, disj_elim 3 5 19.
rle_lt_tricho. ⊢ a ∈ ℝ → b ∈ ℝ → a ≤ b ∨ b < a,
  subj_intro_ii 20.

Dependencies
The given proof depends on six axioms:
efq, eq_refl, eq_subst, lem, rle_refl, rle_total.