theorem :: QUATERN3:41

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