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

end;

case b >= a ; :: thesis: contradiction

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

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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