let n be Element of NAT ; :: thesis: for z1, z2, z being Element of COMPLEX n holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
let z1, z2, z be Element of COMPLEX n; :: thesis: |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
|.(z1 - z2).| = |.(((z1 - z) + z) - z2).| by Th51
.= |.((z1 - z) + (z - z2)).| by Th46 ;
hence |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| by Th68; :: thesis: verum