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

end;

case b >= a ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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