theorem Th2: :: EUCLID_3:2

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