let x be real number ; :: thesis: ( 1 <= x implies (x ^2 ) - 1 >= 0 )
assume 1 <= x ; :: thesis: (x ^2 ) - 1 >= 0
then x ^2 >= 1 ^2 by SQUARE_1:77;
then 1 + (- 1) <= (x ^2 ) + (- 1) by XREAL_1:8;
hence (x ^2 ) - 1 >= 0 ; :: thesis: verum