theorem Th9: :: SIN_COS7:9

for x, y being Real st y >= 0 & x >= 1 holds
((x ^2) - 1) / y >= 0