MetrStruct(# the carrier of TarskiEuclid2Space, the distance of TarskiEuclid2Space #) = MetrStruct(# the carrier of (Euclid 2), the distance of (Euclid 2) #) by GTARSKI1:def 13;
hence RP3_to_REAL2 P is Point of TarskiEuclid2Space ; :: thesis: verum