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