let a, b, c be Real; :: thesis: ( a - b <= c implies a <= b + c )
assume a - b <= c ; :: thesis: a <= b + c
then (a - b) + b <= c + b by Lm5;
hence a <= b + c ; :: thesis: verum