theorem Th7: :: SIN_COS7:7
for x, y being Real st y >= 0 & x >= 1 holds
(x - 1) / y >= 0