let k, m be Element of NAT ; :: thesis: ( k < m iff k <= m - 1 )
A1: now :: thesis: ( k <= m - 1 implies k < m )
assume k <= m - 1 ; :: thesis: k < m
then A2: k + 1 <= m by XREAL_1:19;
k < k + 1 by XREAL_1:29;
hence k < m by A2, XXREAL_0:2; :: thesis: verum
end;
now :: thesis: ( k < m implies k <= m - 1 )
assume k < m ; :: thesis: k <= m - 1
then k + 1 <= m by INT_1:7;
hence k <= m - 1 by XREAL_1:19; :: thesis: verum
end;
hence ( k < m iff k <= m - 1 ) by A1; :: thesis: verum