theorem Th2: :: QUATERN2:2
for c1, c2, c3 being Quaternion holds (c1 + c2) + c3 = c1 + (c2 + c3)