theorem Th19: :: QUATERN2:19

for c being Quaternion holds - c = (- 1q) * c