let z1, z2 be Quaternion; :: thesis: |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z2 - z1).|) / 2
( |.(z1 + z2).| <= |.z1.| + |.z2.| & |.(z1 - z2).| <= |.z1.| + |.z2.| ) by QUATERNI:79, QUATERNI:80;
then |.(z1 + z2).| + |.(z1 - z2).| <= (|.z1.| + |.z2.|) + (|.z1.| + |.z2.|) by XREAL_1:7;
then |.(z1 + z2).| + |.(z2 - z1).| <= 2 * (|.z1.| + |.z2.|) by QUATERNI:83;
hence |.z1.| + |.z2.| >= (|.(z1 + z2).| + |.(z2 - z1).|) / 2 by XREAL_1:79; :: thesis: verum