let z1, z2 be complex number ; :: 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 ( 0 <= |.(z1 - z2).| & |.(z1 - z2).| <> 0 ) by Th132, Th147;
hence 0 < |.(z1 - z2).| ; :: thesis: verum

end;

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