let z1, z2 be Element of F_Complex; :: thesis: ( z1 <> z2 iff 0 < |.(z1 - z2).| )
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
thus ( z1 <> z2 implies 0 < |.(z1 - z2).| ) :: thesis: ( 0 < |.(z1 - z2).| implies z1 <> z2 )

proof

assume A1: z1 <> z2 ; :: thesis: 0 < |.(z1 - z2).|
z1 - z2 = z19 - z29 by Th3;
hence 0 < |.(z1 - z2).| by A1, COMPLEX1:62; :: thesis: verum

end;

assume A2: 0 < |.(z1 - z2).| ; :: thesis: z1 <> z2
z1 - z2 = z19 - z29 by Th3;
hence z1 <> z2 by A2; :: thesis: verum