theorem :: EUCLID_3:18

for p being Point of (TOP-REAL 2) st euc2cpx p = 0c holds
p = 0. (TOP-REAL 2) by Th2, Th16;