theorem :: QUATERN2:6

for c1, c2, c3 being Quaternion holds (c1 - c2) + c3 = (c1 + c3) - c2 by Th2;