theorem :: BHSP_1:38

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