let z1, z2 be Complex; :: thesis: |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|
|.z2.| - |.z1.| <= |.(z2 - z1).| by Th59;
then - (|.z1.| - |.z2.|) <= |.(z1 - z2).| by Th60;
then A1: - |.(z1 - z2).| <= - (- (|.z1.| - |.z2.|)) by XREAL_1:24;
|.z1.| - |.z2.| <= |.(z1 - z2).| by Th59;
hence |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by A1, Lm30; :: thesis: verum