let a, b, c be real number ; :: thesis: ( a <= 0 & b <= c implies b <= c - a )
assume that
A1: a <= 0 and
A2: b <= c ; :: thesis: b <= c - a
b + a <= c by A1, A2, Th37;
hence b <= c - a by Lm16; :: thesis: verum