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