theorem Th4: :: SIN_COS7:4

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