theorem :: QUATERNI:81

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