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