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