let z1, z2, z3 be quaternion number ; :: thesis: |.((z1 + z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.|
A1: |.((z1 + z2) - z3).| = |.(z1 + (z2 - z3)).| by QUATERN2:2;
A2: |.((z1 + z2) - z3).| <= |.z1.| + |.(z2 - z3).| by A1, QUATERNI:79;
A3: |.((z1 + z2) - z3).| - |.z1.| <= |.(z2 - z3).| by A2, XREAL_1:22;
A4: |.(z2 - z3).| <= |.z2.| + |.z3.| by QUATERNI:80;
A5: (|.((z1 + z2) - z3).| - |.z1.|) + |.(z2 - z3).| <= |.(z2 - z3).| + (|.z2.| + |.z3.|) by A3, A4, XREAL_1:9;
A6: |.((z1 + z2) - z3).| - |.z1.| <= (|.(z2 - z3).| + (|.z2.| + |.z3.|)) - |.(z2 - z3).| by A5, XREAL_1:21;
A7: |.((z1 + z2) - z3).| <= (|.z2.| + |.z3.|) + |.z1.| by A6, XREAL_1:22;
thus |.((z1 + z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| by A7; :: thesis: verum