theorem :: COMPTRIG:2

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