let k, m be Integer; :: thesis: ( k < m + 1 iff k <= m )
( k < m + 1 iff k - 1 < m ) by XREAL_1:19;
hence ( k < m + 1 iff k <= m ) by Lm8; :: thesis: verum