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