theorem Th57: :: COMPLEX1:57

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