ile_lt_trans

Theorem. ile_lt_trans
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a ≤ b → b < c → a < c

Proof
ile_lt_trans. ⊢ a ∈ ℤ → b ∈ ℤ → c ∈ ℤ →
  a ≤ b → b < c → a < c,
  pred_iii_restr int_incl_in_real rle_lt_trans.

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