let a, b be Real; :: 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 :: thesis: ( not - a > b & not b > a )

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

now :: thesis: ( ( - a > b & contradiction ) or ( b > a & contradiction ) )

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, Th16;
hence contradiction by A1; :: thesis: verum

end;

case b > a ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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