theorem Th22: :: QUATERN2:22

for c1, c2 being Quaternion holds (- c1) * (- c2) = c1 * c2