theorem :: SIN_COS7:20

for x being Real st 0 < x & x < 1 holds
(1 + (x ^2)) / (1 - (x ^2)) > 1