theorem :: CSSPACE:55

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