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 Lm8;
hence c + a < b ; :: thesis: verum