let a, b be real number ; :: thesis: ( 0 <= a & (b - a) * (b + a) < 0 implies ( - a < b & b < a ) )
assume A1: ( a >= 0 & (b - a) * (b + a) < 0 ) ; :: thesis: ( - a < b & b < a )
then A2: ( ( b - a > 0 & b + a < 0 ) or ( b - a < 0 & b + a > 0 ) ) by Lm44;
A3: b + 0 <= b + a by A1, Lm6;
then b - a <= (b + a) - a by Lm7;
then ( b < a + 0 & b + a > 0 ) by A2, A3, Lm16;
then ( b < a & b > 0 - a ) by Lm17;
hence ( - a < b & b < a ) ; :: thesis: verum