theorem :: QUATERN3:37

for z1, z2, z3 being Quaternion holds |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.|