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