theorem Th13: :: SIN_COS7:13

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