let a be Complex; :: thesis: Im a >= - |.a.|
reconsider b = - a as Complex ;
Im b <= |.b.| by COMPLEX1:55;
then - (Im a) <= - (- |.b.|) by COMPLEX1:17;
then Im a >= - |.(- a).| by XREAL_1:24;
hence Im a >= - |.a.| by COMPLEX1:52; :: thesis: verum