let a, b be Real; :: thesis: ( not 0 <= (b - a) * (b + a) or b <= - a or a <= b )
assume (b - a) * (b + a) >= 0 ; :: thesis: ( b <= - a or a <= b )
then ( ( b - a >= 0 & b + a >= 0 ) or ( b - a <= 0 & b + a <= 0 ) ) ;
then ( (b - a) + a >= 0 + a or b + a <= 0 ) by Lm6;
then ( b >= 0 + a or (b + a) - a <= 0 - a ) by Lm7;
hence ( b <= - a or a <= b ) ; :: thesis: verum