theorem :: COMPLEX1:58

for z1, z2 being Complex holds |.z1.| - |.z2.| <= |.(z1 + z2).|