for p1, p2 being Point of (TOP-REAL 2) holds |(p1,p2)| = Re ((euc2cpx p1) .|. (euc2cpx p2))