:: deftheorem defines dist BHSP_1:def 5 :
for X being RealUnitarySpace
for x, y being Point of X holds dist (x,y) = ||.(x - y).||;