let p be Point of (TOP-REAL 2); :: thesis: ex x, y being Real st p = <*x,y*>
TopStruct(# the carrier of (TOP-REAL 2),the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by Def8;
then p is Tuple of 2, REAL by FINSEQ_2:151;
hence ex x, y being Real st p = <*x,y*> by FINSEQ_2:120; :: thesis: verum