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