let x, y be Element of COMPLEX ; :: thesis: (- x) .|. y = x .|. (- y)
thus (- x) .|. y = (- (1r *')) * (x .|. y) by COMPLEX1:30, COMPLEX1:def 4
.= ((- 1r) *') * (x .|. y) by COMPLEX1:33
.= x .|. ((- 1r) * y) by Th51
.= x .|. (- y) by COMPLEX1:def 4 ; :: thesis: verum