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