theorem :: COMPLFLD:64

for z1, z2 being Element of F_Complex holds |.z1.| - |.z2.| <= |.(z1 + z2).| by COMPLEX1:58;