for X being ComplexUnitarySpace
for x, y being Point of X holds
( x <> y iff dist (x,y) > 0 )