theorem Th31: :: SIN_COS7:31

for t being Real holds ((t ^2) - 1) / ((t ^2) + 1) < 1