theorem Th34: :: BHSP_1:34

for X being RealUnitarySpace
for x being Point of X holds dist (x,x) = 0