theorem :: COMPLEX1:62

for z1, z2 being Complex holds
( z1 <> z2 iff 0 < |.(z1 - z2).| )