theorem :: QUATERNI:81

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