let z, z1, z2 be Element of F_Complex; :: thesis: |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
reconsider z9 = z, z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
A1: z9 - z29 = z - z2 by Th3;
( |.(z19 - z29).| = |.(z1 - z2).| & |.(z19 - z9).| = |.(z1 - z).| ) by Th3;
hence |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| by A1, COMPLEX1:63; :: thesis: verum