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