theorem COMPLEX154a: :: COMPLEX3:4

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