theorem Th10: :: SIN_COS7:10

for x being Real st x >= 1 holds
(sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0