theorem :: COMPLFLD:70

for z1, z2 being Element of F_Complex holds |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|