let z1, z2 be Element of F_Complex; :: thesis: |.(z1 - z2).| = |.(z2 - z1).|
reconsider z19 = z1, z29 = z2 as Element of COMPLEX by Def1;
( z29 - z19 = z2 - z1 & z19 - z29 = z1 - z2 ) by Th3;
hence |.(z1 - z2).| = |.(z2 - z1).| by COMPLEX1:60; :: thesis: verum