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) = (- z1) + (- (- z2)) by Th65
.= z2 - z1 ; :: thesis: verum