let n be 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 Th70
.= |.(z2 - z1).| by Th90 ; :: thesis: verum