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