let n be Element of NAT ; :: thesis: for z1, z2 being Element of COMPLEX n holds |.(z1 - z2).| = |.(z2 - z1).|
let z1, z2 be Element of COMPLEX n; :: thesis: |.(z1 - z2).| = |.(z2 - z1).|
thus |.(z1 - z2).| = |.(- (z2 - z1)).| by Th88
.= |.(z2 - z1).| by Th108 ; :: thesis: verum