theorem Th70: :: QUATERN3:70

for z1, z2, z3, z4 being Quaternion holds ((z1 - z2) - z3) + z4 = ((z4 - z3) - z2) + z1