assume |.z.| is zero ; :: thesis: contradiction
then ((Re z) ^2) + ((Im z) ^2) = 0 by Lm1, SQUARE_1:24;
hence contradiction by Th5; :: thesis: verum