let a, b be Real; :: thesis: ( a <= b implies a - 1 < b )
assume a <= b ; :: thesis: a - 1 < b
then A1: a - 1 <= b - 1 by Lm7;
b - 1 < (b - 1) + 1 by Lm9;
hence a - 1 < b by A1, XXREAL_0:2; :: thesis: verum