let x be Real; :: thesis: ( 1 <= x implies (x ^2) - 1 >= 0 )
assume 1 <= x ; :: thesis: (x ^2) - 1 >= 0
then x ^2 >= 1 ^2 by SQUARE_1:15;
then 1 + (- 1) <= (x ^2) + (- 1) by XREAL_1:6;
hence (x ^2) - 1 >= 0 ; :: thesis: verum