theorem :: QUATERN3:71
for z1, z2, z3, z4 being Quaternion holds (z1 - z2) * (z3 - z4) = (z2 - z1) * (z4 - z3)