let x be real number ; :: thesis: ( x > 1 implies ((sqrt ((x ^2 ) - 1)) / x) ^2 < 1 )
assume x > 1 ; :: thesis: ((sqrt ((x ^2 ) - 1)) / x) ^2 < 1
then x ^2 > (1 ^2 ) + 0 by SQUARE_1:78;
then A1: (x ^2 ) - 1 > 0 by XREAL_1:22;
A2: (- 1) + (x ^2 ) < 0 + (x ^2 ) by XREAL_1:8;
((sqrt ((x ^2 ) - 1)) / x) ^2 = ((sqrt ((x ^2 ) - 1)) ^2 ) / (x ^2 ) by XCMPLX_1:77
.= ((x ^2 ) - 1) / (x ^2 ) by A1, SQUARE_1:def 4 ;
hence ((sqrt ((x ^2 ) - 1)) / x) ^2 < 1 by A1, A2, XREAL_1:191; :: thesis: verum