let z be Complex; :: thesis: Im z <= |.z.|
0 <= (Re z) ^2 by XREAL_1:63;
then A1: ((Im z) ^2) + 0 <= ((Re z) ^2) + ((Im z) ^2) by XREAL_1:7;
0 <= (Im z) ^2 by XREAL_1:63;
then sqrt ((Im z) ^2) <= |.z.| by A1, SQUARE_1:26;
then A2: |.(Im z).| <= |.z.| by Lm28;
Im z <= |.(Im z).| by Lm29;
hence Im z <= |.z.| by A2, XXREAL_0:2; :: thesis: verum