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