let z1, z2 be quaternion number ; :: thesis: |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|
|.z2.| - |.z1.| <= |.(z2 - z1).| by Th82;
then - (|.z1.| - |.z2.|) <= |.(z1 - z2).| by Th83;
then A1: - |.(z1 - z2).| <= - (- (|.z1.| - |.z2.|)) by XREAL_1:24;
|.z1.| - |.z2.| <= |.(z1 - z2).| by Th82;
hence |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by A1, ABSVALUE:5; :: thesis: verum