let m, n, k be Nat; :: thesis: ( m < n & n <= k + 1 implies m <= k )
assume that
A1: m < n and
A2: n <= k + 1 ; :: thesis: m <= k
m + 1 <= n by A1, NAT_1:13;
then m + 1 <= k + 1 by A2, XXREAL_0:2;
hence m <= k by XREAL_1:6; :: thesis: verum