let z1, z2, z be Quaternion; :: thesis: |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).|
( |.z1.| - |.z2.| <= |.(z1 - z2).| & |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| ) by QUATERNI:82, QUATERNI:85;
then (|.z1.| - |.z2.|) + |.(z1 - z2).| <= |.(z1 - z2).| + (|.(z1 - z).| + |.(z - z2).|) by XREAL_1:7;
then |.z1.| - |.z2.| <= ((|.(z1 - z2).| + |.(z1 - z).|) + |.(z - z2).|) - |.(z1 - z2).| by XREAL_1:19;
hence |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).| ; :: thesis: verum