MetrStruct(# the U1 of (TarskiEuclidSpace n), the distance of (TarskiEuclidSpace n) #) = MetrStruct(# the U1 of (Euclid n), the distance of (Euclid n) #) by GTARSKI1:def 13;
hence P is Element of (TOP-REAL n) by EUCLID:22; :: thesis: verum