0 <= ((Re z) ^2 ) + ((Im z) ^2 ) by Lm1;
hence not |.z.| is negative by SQUARE_1:def 4; :: thesis: verum