let z1, z2 be quaternion number ; :: thesis: |.(z1 - z2).| <= |.z1.| + |.z2.|
|.(z1 - z2).| <= |.z1.| + |.(- z2).| by Th79;
hence |.(z1 - z2).| <= |.z1.| + |.z2.| by Th72; :: thesis: verum