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