:: deftheorem defines dist RSSPACE3:def 4 :
for X being non empty NORMSTR
for x, y being Point of X holds dist (x,y) = ||.(x - y).||;