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 Lm10;
hence b < b - a by Lm19; :: thesis: verum