let a, b be Real; :: thesis: ( 0 <= a & (b - a) * (b + a) <= 0 implies ( - a <= b & b <= a ) )
assume that
A1: a >= 0 and
A2: (b - a) * (b + a) <= 0 ; :: thesis: ( - a <= b & b <= a )
b + 0 <= b + a by A1, Lm6;
then b + a >= 0 by A1, A2;
then A3: b >= 0 - a by Lm18;
( ( b - a >= 0 & b + a <= 0 ) or ( b - a <= 0 & b + a >= 0 ) ) by A2;
then b <= a + 0 by A1, Lm19;
hence ( - a <= b & b <= a ) by A3; :: thesis: verum