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:11;
then (a - 1) + 1 <= b - 1 by Th20;
hence a <= b - 1 ; :: thesis: verum