let a, b, c be Real; :: thesis: ( a <= 0 & c <= b implies c + a <= b )
assume that
A1: a <= 0 and
A2: c <= b ; :: thesis: c + a <= b
a + c <= 0 + b by A1, A2, Lm6;
hence c + a <= b ; :: thesis: verum