let n be Element of NAT ; :: thesis: ( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n )
( Euclid n = MetrStruct(# (REAL n),(Pitag_dist n) #) & TOP-REAL n = TopSpaceMetr (Euclid n) ) by EUCLID:def 7, EUCLID:def 8;
hence ( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n ) by TOPMETR:16; :: thesis: verum