let z1, z2 be Complex; :: thesis: |.(z1 - z2).| <= |.z1.| + |.z2.|
|.(z1 - z2).| = |.(z1 + (- z2)).| ;
then |.(z1 - z2).| <= |.z1.| + |.(- z2).| by Th56;
hence |.(z1 - z2).| <= |.z1.| + |.z2.| by Lm26; :: thesis: verum