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