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