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 Th16; :: thesis: verum