theorem COMPLEX155a: :: COMPLEX3:5

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