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