let p be Point of (TOP-REAL 2); :: thesis: euc2cpx (- p) = - (euc2cpx p)
- (euc2cpx p) = (- (p `1)) + ((- (p `2)) * <i>) ;
hence euc2cpx (- p) = - (euc2cpx p) by Th12; :: thesis: verum