theorem :: BHSP_1:39

for X being RealUnitarySpace
for x, y being Point of X holds dist (x,y) = sqrt ((x - y) .|. (x - y)) ;