theorem Th18: :: SIN_COS7:18
for x being Real st 0 < x & x < 1 holds
(2 * x) / (1 - (x ^2)) > 0