let x, y be Complex; :: thesis: (- x) .|. (- y) = x .|. y
(- x) .|. (- y) = - (x .|. (- y))
.= - (- (x .|. y)) by Th42 ;
hence (- x) .|. (- y) = x .|. y ; :: thesis: verum