theorem Th34: :: BHSP_1:34
for X being RealUnitarySpace
for x being Point of X holds dist (x,x) = 0