let x, a be real number ; :: thesis: ( abs x <= a implies x ^2 <= a ^2 )
assume A1: abs x <= a ; :: thesis: x ^2 <= a ^2

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

suppose A2: x >= 0 ; :: thesis: x ^2 <= a ^2

x <= a by A1, ABSVALUE:def 1;
hence x ^2 <= a ^2 by A2, SQUARE_1:15; :: thesis: verum

end;

suppose A3: x < 0 ; :: thesis: x ^2 <= a ^2

then - x <= a by A1, ABSVALUE:def 1;
then (- x) ^2 <= a ^2 by A3, SQUARE_1:15;
hence x ^2 <= a ^2 ; :: thesis: verum

end;

end;