theorem :: SIN_COS7:21

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