theorem Th54: :: QUATERN3:54
for z1, z2, z being Quaternion holds z - (z1 + z2) = (z - z1) - z2