for p being Point of (TOP-REAL 2) holds cpx2euc (euc2cpx p) = p