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 = (z1 - z2) + z2 by Th80;
then |.z1.| <= |.(z1 - z2).| + |.z2.| by Th97;
hence |.z1.| - |.z2.| <= |.(z1 - z2).| by XREAL_1:20; :: thesis: verum