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