let z1, z2 be Complex; :: thesis: ( z1 <> z2 iff 0 < |.(z1 - z2).| )
thus ( z1 <> z2 implies 0 < |.(z1 - z2).| ) :: thesis: ( 0 < |.(z1 - z2).| implies z1 <> z2 )

proof

assume z1 <> z2 ; :: thesis: 0 < |.(z1 - z2).|
then |.(z1 - z2).| <> 0 by Th61;
hence 0 < |.(z1 - z2).| ; :: thesis: verum

end;

thus ( 0 < |.(z1 - z2).| implies z1 <> z2 ) ; :: thesis: verum