let a, b be real number ; :: thesis: ( 0 <= a & 0 <= (b - a) * (b + a) & not b <= - a implies a <= b )
assume ( a >= 0 & (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