theorem :: COMPLFLD:68

for z1, z2 being Element of F_Complex holds
( z1 <> z2 iff 0 < |.(z1 - z2).| )