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