theorem Th20: :: CSSPACE:25

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