let z1, z2, z3 be quaternion number ; :: thesis: |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.|
A1: |.((z1 - z2) - z3).| <= |.(z1 - z2).| + |.z3.| by QUATERNI:80;
|.(z1 - z2).| <= |.z1.| + |.z2.| by QUATERNI:80;
then |.((z1 - z2) - z3).| + |.(z1 - z2).| <= (|.(z1 - z2).| + |.z3.|) + (|.z1.| + |.z2.|) by A1, XREAL_1:9;
then |.((z1 - z2) - z3).| <= ((|.(z1 - z2).| + |.z3.|) + (|.z1.| + |.z2.|)) - |.(z1 - z2).| by XREAL_1:21;
hence |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| ; :: thesis: verum