theorem Th25: :: SIN_COS7:25

for y being Real st 1 <= y holds
0 < y - (sqrt ((y ^2) - 1))