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