let z1, z2 be Element of F_Complex; :: thesis: |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
z19 - z29 = z1 - z2 by Th3;
hence |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by COMPLEX1:64; :: thesis: verum