let z1, z2 be quaternion number ; :: thesis: |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z1 - z2).|) / 2
A1: ( |.z1.| - |.z2.| <= |.(z1 + z2).| & |.z1.| - |.z2.| <= |.(z1 - z2).| ) by QUATERNI:81, QUATERNI:82;
A2: (|.z1.| - |.z2.|) + (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z1 - z2).| by A1, XREAL_1:9;
A3: 2 * (|.z1.| - |.z2.|) <= |.(z1 + z2).| + |.(z1 - z2).| by A2;
thus |.z1.| - |.z2.| <= (|.(z1 + z2).| + |.(z1 - z2).|) / 2 by A3, XREAL_1:79; :: thesis: verum