theorem :: SIN_COS7:17

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