theorem :: SIN_COS7:2

for x being Real st x > 1 holds
((sqrt ((x ^2) - 1)) / x) ^2 < 1