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