let z1, z2 be complex number ; :: thesis: |.z1.| - |.z2.| <= |.(z1 + z2).|
z1 = (z1 + z2) - z2 ;
then |.z1.| <= |.(z1 + z2).| + |.z2.| by Th143;
hence |.z1.| - |.z2.| <= |.(z1 + z2).| by XREAL_1:22; :: thesis: verum