let p be Point of (TOP-REAL 2); :: thesis: p is Point of (Euclid 2)
TopSpaceMetr (Euclid 2) = TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by EUCLID:def 8;
then TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopStruct(# the carrier of (Euclid 2),(Family_open_set (Euclid 2)) #) by PCOMPS_1:def 5;
hence p is Point of (Euclid 2) ; :: thesis: verum