theorem :: QUATERN2:34

for c being Quaternion holds (- c) " = - (c ")