MetrStruct(# the U1 of TarskiEuclid2Space, the distance of TarskiEuclid2Space #) = MetrStruct(# the U1 of (Euclid 2), the distance of (Euclid 2) #) by GTARSKI1:def 13;
hence P is Element of REAL 2 ; :: thesis: verum