:: deftheorem defines dist CSSPACE:def 16 :
for X being ComplexUnitarySpace
for x, y being Point of X holds dist (x,y) = ||.(x - y).||;