let z1, z2, z be Element of F_Complex ; :: thesis: |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
reconsider z' = z, z1' = z1, z2' = z2 as Element of COMPLEX by Def1;
A1: |.(z1' - z2').| = |.(z1 - z2).| by Th5;
A2: |.(z1' - z').| = |.(z1 - z).| by Th5;
z' - z2' = z - z2 by Th5;
hence |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| by A1, A2, COMPLEX1:149; :: thesis: verum