for X being ComplexUnitarySpace
for x, y being Point of X holds dist (x,y) >= 0 by Th39;