theorem Th20: :: QUATERN2:20

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