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