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 x <> y ; :: thesis: dist (x,y) > 0
then dist (x,y) <> 0 by Th47;
hence dist (x,y) > 0 by Th39; :: thesis: verum

end;

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