let X be ComplexUnitarySpace; :: thesis: for x, y being Point of X holds
( x <> y iff dist (x,y) <> 0 )
let x, y be Point of X; :: thesis: ( x <> y iff dist (x,y) <> 0 )
thus ( x <> y implies dist (x,y) <> 0 ) :: thesis: ( dist (x,y) <> 0 implies x <> y )

proof

assume that
A1: x <> y and
A2: dist (x,y) = 0 ; :: thesis: contradiction
x - y = H₁(X) by A2, Th37;
hence contradiction by A1, RLVECT_1:21; :: thesis: verum

end;

thus ( dist (x,y) <> 0 implies x <> y ) by Th45; :: thesis: verum