let x, y be Element of COMPLEX ; :: thesis: (- x) .|. (- y) = x .|. y
(- x) .|. (- y) = - (x .|. (- y))
.= - (- (x .|. y)) by Th57 ;
hence (- x) .|. (- y) = x .|. y ; :: thesis: verum