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 <= (c + b) - b by Lm7;
hence a - b <= c ; :: thesis: verum