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