theorem Th8: :: SIN_COS7:8

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