for z1, z2 being Complex st (Re z1) * (Im z2) = (Re z2) * (Im z1) & ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) >= 0 holds
|.(z1 + z2).| = |.z1.| + |.z2.| by Lm3;