theorem Th56: :: COMPLEX1:56
for z1, z2 being Complex holds |.(z1 + z2).| <= |.z1.| + |.z2.|