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, Th15; :: 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, Th15;
hence b ^2 <= a ^2 ; :: thesis: verum

end;

end;