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