theorem Th25: :: EUCLID_3:25

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