let z, z1, z2 be Quaternion; :: thesis: |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
|.(z1 - z2).| = |.((z1 - z) + (z - z2)).| by Lm39;
hence |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| by Th72; :: thesis: verum