let z be complex number ; :: thesis: 0 <= |.z.|
0 <= ((Re z) ^2 ) + ((Im z) ^2 ) by Lm1;
hence 0 <= |.z.| by SQUARE_1:def 4; :: thesis: verum