let k, l, m be Nat; :: thesis: ( l + m <= k - 1 implies ( l < k & m < k ) )
assume A1: l + m <= k - 1 ; :: thesis: ( l < k & m < k )
then A2: (l + m) - m <= (k - 1) - m by XREAL_1:9;
k <= k + m by NAT_1:11;
then A3: k - m <= (k + m) - m by XREAL_1:9;
(k - 1) - m = (k - m) - 1 ;
then (k - 1) - m < k by A3, XREAL_1:146, XXREAL_0:2;
hence l < k by A2, XXREAL_0:2; :: thesis: m < k
k <= k + l by NAT_1:11;
then A4: k - l <= (k + l) - l by XREAL_1:9;
A5: (m + l) - l <= (k - 1) - l by A1, XREAL_1:9;
(k - 1) - l = (k - l) - 1 ;
then (k - 1) - l < k by A4, XREAL_1:146, XXREAL_0:2;
hence m < k by A5, XXREAL_0:2; :: thesis: verum