theorem :: COMPLFLD:66

for z1, z2 being Element of F_Complex holds |.(z1 - z2).| = |.(z2 - z1).|