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