let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( euc2cpx p1 = euc2cpx p2 implies p1 = p2 )
assume A1: euc2cpx p1 = euc2cpx p2 ; :: thesis: p1 = p2
p2 = cpx2euc (euc2cpx p2) by Th2;
hence p1 = p2 by A1, Th2; :: thesis: verum