theorem :: BHSP_1:37

for X being RealUnitarySpace
for x, y being Point of X holds dist (x,y) >= 0 by Th28;