let z1, z2 be complex number ; :: thesis: |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|
|.z2.| - |.z1.| <= |.(z2 - z1).| by Th145;
then - (|.z1.| - |.z2.|) <= |.(z1 - z2).| by Th146;
then - |.(z1 - z2).| <= - (- (|.z1.| - |.z2.|)) by XREAL_1:26;
then ( - |.(z1 - z2).| <= |.z1.| - |.z2.| & |.z1.| - |.z2.| <= |.(z1 - z2).| ) by Th145;
hence |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by Lm26; :: thesis: verum