theorem :: QUATERN2:55
for c1, c2 being Quaternion holds (- c1) .|. c2 = - (c1 .|. c2) by Th20;