theorem Th1: :: COMPTRIG:1

for z being Complex holds Re z >= - |.z.|