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