let c1, c2 be Quaternion; :: thesis: (- c1) .|. (- c2) = c1 .|. c2
(- c1) .|. (- c2) = (- c1) * (- (c2 *')) by QUATERNI:55
.= c1 * (c2 *') by Th22 ;
hence (- c1) .|. (- c2) = c1 .|. c2 ; :: thesis: verum