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