ilt_lt_trans

Theorem. ilt_lt_trans
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a < b → b < c → a < c

Proof
ilt_lt_trans. ⊢ a ∈ ℤ → b ∈ ℤ → c ∈ ℤ →
  a < b → b < c → a < c,
  pred_iii_restr int_incl_in_real rlt_lt_trans.

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