theorem Th36: :: BHSP_1:36

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