theorem Th40: :: COMPLEX2:42

for x, y being Complex holds (- x) .|. y = x .|. (- y)