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