let z1, z2 be quaternion number ; :: thesis: |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).|
A1: |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by QUATERNI:86;
thus |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).| by A1, QUATERNI:83; :: thesis: verum