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