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