let z1, z2 be Quaternion; :: thesis: |.z1.| - |.z2.| <= |.(z1 + z2).|
z1 = (z1 + z2) - z2 by Lm34;
then |.z1.| <= |.(z1 + z2).| + |.z2.| by Th73;
hence |.z1.| - |.z2.| <= |.(z1 + z2).| by XREAL_1:20; :: thesis: verum