theorem Th26: :: SIN_COS7:26

for x, y being Real st 1 <= x & 1 <= y & |.y.| <= |.x.| holds
0 <= (y * (sqrt ((x ^2) - 1))) - (x * (sqrt ((y ^2) - 1)))