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

now

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

now

per cases ( - a >= b or b >= a ) by A2;

case - a >= b ; :: thesis: contradiction

then - (- a) <= - b by XREAL_1:26;
then a ^2 <= (- b) ^2 by A1, Th77;
hence contradiction by A1; :: thesis: verum

end;

case b >= a ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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