theorem Th5: :: SIN_COS7:5

for x being Real holds (sqrt ((x ^2) + 1)) + x > 0