theorem Th13: :: EUCLID_3:13

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