for p being Point of (Euclid 2)
for q being Point of (TOP-REAL 2) st p = 0. (TOP-REAL 2) & p = q holds
( q = <*0,0*> & q `1 = 0 & q `2 = 0 )