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