let z1, z2 be Quaternion; :: thesis: |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|
|.z2.| - |.z1.| <= |.(z2 - z1).| by Th75;
then - (|.z1.| - |.z2.|) <= |.(z1 - z2).| by Th76;
then A1: - |.(z1 - z2).| <= - (- (|.z1.| - |.z2.|)) by XREAL_1:24;
|.z1.| - |.z2.| <= |.(z1 - z2).| by Th75;
hence |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by A1, ABSVALUE:5; :: thesis: verum