theorem Th23: :: SIN_COS7:23

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