let z1, z2 be Quaternion; :: thesis: |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).|
|.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by QUATERNI:86;
hence |.(|.z1.| - |.z2.|).| <= |.(z2 - z1).| by QUATERNI:83; :: thesis: verum