let z1, z2 be quaternion number ; :: thesis: |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z2 - z1).|) / 2
A: |.z1.| - |.z2.| <= |.(z1 + z2).| by QUATERNI:81;
|.z1.| - |.z2.| <= |.(z1 - z2).| by QUATERNI:82;
then (|.z1.| - |.z2.|) + (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z1 - z2).| by XREAL_1:9, A;
then 2 * (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z2 - z1).| by QUATERNI:83;
hence |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 by XREAL_1:79; :: thesis: verum