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