let a be positive Real; :: thesis: for x being Real st |.x.| >= a holds
x ^2 >= a ^2
let x be Real; :: thesis: ( |.x.| >= a implies x ^2 >= a ^2 )
assume A1: |.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;