rlt_lt_trans

Theorem rlt_lt_trans

Theorem. rlt_lt_trans
a ∈ ℝ → b ∈ ℝ → c ∈ ℝ → a < b → b < c → a < c

Proof
01. 1 ⊢ a ∈ ℝ, hypo.
02. 2 ⊢ b ∈ ℝ, hypo.
03. 3 ⊢ c ∈ ℝ, hypo.
04. 4 ⊢ a < b, hypo.
05. 5 ⊢ b < c, hypo.
06. 4 ⊢ a ≤ b, le_from_lt 4.
07. 1, 2, 3, 4, 5 ⊢ a < c, rle_lt_trans 1 2 3 6 5.
08. 1, 2, 3 ⊢ a < b → b < c → a < c, subj_intro_ii 7.
rlt_lt_trans. ⊢ a ∈ ℝ → b ∈ ℝ → c ∈ ℝ →
  a < b → b < c → a < c, subj_intro_iii 8.

Dependencies
The given proof depends on four axioms:
eq_refl, eq_subst, rle_antisym, rle_trans.