let a, b be Integer; :: thesis: ( a < b implies a <= b - 1 )
assume a < b ; :: thesis: a <= b - 1
then a - 1 < b - 1 by XREAL_1:9;
then (a - 1) + 1 <= b - 1 by Th7;
hence a <= b - 1 ; :: thesis: verum