let z1, z2, z3 be Quaternion; :: thesis: |.((z1 + z2) + z3).| <= (|.z1.| + |.z2.|) + |.z3.|
|.((z1 + z2) + z3).| = |.(z1 + (z2 + z3)).| by QUATERN2:2;
then |.((z1 + z2) + z3).| <= |.z1.| + |.(z2 + z3).| by QUATERNI:79;
then A1: |.((z1 + z2) + z3).| - |.z1.| <= |.(z2 + z3).| by XREAL_1:20;
|.(z2 + z3).| <= |.z2.| + |.z3.| by QUATERNI:79;
then (|.((z1 + z2) + z3).| - |.z1.|) + |.(z2 + z3).| <= |.(z2 + z3).| + (|.z2.| + |.z3.|) by A1, XREAL_1:7;
then |.((z1 + z2) + z3).| - |.z1.| <= (|.(z2 + z3).| + (|.z2.| + |.z3.|)) - |.(z2 + z3).| by XREAL_1:19;
then |.((z1 + z2) + z3).| <= (|.z2.| + |.z3.|) + |.z1.| by XREAL_1:20;
hence |.((z1 + z2) + z3).| <= (|.z1.| + |.z2.|) + |.z3.| ; :: thesis: verum