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 ) ) ;
b + 0 <= b + a by A1, Lm6;
then ( b <= a + 0 & b + a >= 0 ) by A1, A2, Lm19;
then ( b <= a & b >= 0 - a ) by Lm18;
hence ( - a <= b & b <= a ) ; :: thesis: verum