let z be Complex; :: thesis: Re z >= - |.z.|
0 <= (Im z) ^2 by XREAL_1:63;
then A1: ((Re z) ^2) + 0 <= ((Re z) ^2) + ((Im z) ^2) by XREAL_1:7;
0 <= (Re z) ^2 by XREAL_1:63;
then sqrt ((Re z) ^2) <= |.z.| by A1, SQUARE_1:26;
then - (sqrt ((Re z) ^2)) >= - |.z.| by XREAL_1:24;
then ( Re z >= - |.(Re z).| & - |.(Re z).| >= - |.z.| ) by ABSVALUE:4, COMPLEX1:72;
hence Re z >= - |.z.| by XXREAL_0:2; :: thesis: verum