theorem :: COMPLFLD:69

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