let a be real positive number ; :: thesis: for x being real number st abs x >= a holds
x ^2 >= a ^2
let x 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 x >= 0 ; :: thesis: x ^2 >= a ^2

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

end;

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

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

end;

end;