theorem Th75: :: QUATERNI:82

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