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