let b, a be real number ; :: thesis: ( b ^2 <= a ^2 & a >= 0 implies ( - a <= b & b <= a ) )
assume that
A1: b ^2 <= a ^2 and
A2: a >= 0 ; :: thesis: ( - a <= b & b <= a )

now

assume A3: ( - a > b or b > a ) ; :: thesis: contradiction

now

per cases ( - a > b or b > a ) by A3;

case - a > b ; :: thesis: contradiction

then - (- a) < - b by XREAL_1:24;
then a ^2 < (- b) ^2 by A2, Th78;
hence contradiction by A1; :: thesis: verum

end;

case b > a ; :: thesis: contradiction

hence contradiction by A1, A2, Th78; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence ( - a <= b & b <= a ) ; :: thesis: verum