let z be complex number ; :: thesis: cpx2euc (- z) = - (cpx2euc z)
- (cpx2euc z) = |[(- (Re z)),(- (Im z))]| by EUCLID:60;
hence cpx2euc (- z) = - (cpx2euc z) by Th14; :: thesis: verum