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