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