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