let z1, z2 be Element of F_Complex ; :: thesis: ( z1 <> z2 iff 0 < |.(z1 - z2).| )
reconsider z1' = z1, z2' = 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 = z1' - z2' by Th5;
hence 0 < |.(z1 - z2).| by A1, COMPLEX1:148; :: thesis: verum

end;

assume A2: 0 < |.(z1 - z2).| ; :: thesis: z1 <> z2
z1 - z2 = z1' - z2' by Th5;
hence z1 <> z2 by A2, COMPLEX1:148; :: thesis: verum