let x be Real; :: thesis: ( x > 1 implies ((sqrt ((x ^2) - 1)) / x) ^2 < 1 )
A1: (- 1) + (x ^2) < 0 + (x ^2) by XREAL_1:6;
assume x > 1 ; :: thesis: ((sqrt ((x ^2) - 1)) / x) ^2 < 1
then x ^2 > (1 ^2) + 0 by SQUARE_1:16;
then A2: (x ^2) - 1 > 0 by XREAL_1:20;
((sqrt ((x ^2) - 1)) / x) ^2 = ((sqrt ((x ^2) - 1)) ^2) / (x ^2) by XCMPLX_1:76
.= ((x ^2) - 1) / (x ^2) by A2, SQUARE_1:def 2 ;
hence ((sqrt ((x ^2) - 1)) / x) ^2 < 1 by A2, A1, XREAL_1:189; :: thesis: verum