let z1, z2, z3 be Quaternion; :: thesis: |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.|
( |.((z1 - z2) - z3).| <= |.(z1 - z2).| + |.z3.| & |.(z1 - z2).| <= |.z1.| + |.z2.| ) by QUATERNI:80;
then |.((z1 - z2) - z3).| + |.(z1 - z2).| <= (|.(z1 - z2).| + |.z3.|) + (|.z1.| + |.z2.|) by XREAL_1:7;
then |.((z1 - z2) - z3).| <= ((|.(z1 - z2).| + |.z3.|) + (|.z1.| + |.z2.|)) - |.(z1 - z2).| by XREAL_1:19;
hence |.((z1 - z2) - z3).| <= (|.z1.| + |.z2.|) + |.z3.| ; :: thesis: verum