let z1, z2, z be quaternion number ; :: thesis: |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).|
A1: |.z1.| - |.z2.| <= |.(z1 - z2).| by QUATERNI:82;
|.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| by QUATERNI:85;
then (|.z1.| - |.z2.|) + |.(z1 - z2).| <= |.(z1 - z2).| + (|.(z1 - z).| + |.(z - z2).|) by XREAL_1:9, A1;
then |.z1.| - |.z2.| <= ((|.(z1 - z2).| + |.(z1 - z).|) + |.(z - z2).|) - |.(z1 - z2).| by XREAL_1:21;
hence |.z1.| - |.z2.| <= |.(z1 - z).| + |.(z - z2).| ; :: thesis: verum