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