let a, b be Real; :: thesis: ( - a < b & b < a implies b ^2 < a ^2 )
assume that
A1: - a < b and
A2: b < a ; :: thesis: b ^2 < a ^2

per cases ( b >= 0 or b < 0 ) ;

suppose b >= 0 ; :: thesis: b ^2 < a ^2

hence b ^2 < a ^2 by A2, Th16; :: thesis: verum

end;

suppose A3: b < 0 ; :: thesis: b ^2 < a ^2

- (- a) > - b by A1, XREAL_1:24;
then (- b) ^2 < a ^2 by A3, Th16;
hence b ^2 < a ^2 ; :: thesis: verum

end;

end;