let n be Nat; :: thesis: for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| <= |.z1.| + |.z2.|
let z1, z2 be Element of COMPLEX n; :: thesis: |.(z1 - z2).| <= |.z1.| + |.z2.|
|.(z1 - z2).| <= |.z1.| + |.(- z2).| by Th97;
hence |.(z1 - z2).| <= |.z1.| + |.z2.| by Th90; :: thesis: verum