theorem :: EUCLID:51

for p being Point of (TOP-REAL 2) ex x, y being Element of REAL st p = <*x,y*>