let n be 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) #) by EUCLID:def 7;
hence ( the carrier of (Euclid n) = REAL n & the carrier of (TOP-REAL n) = REAL n ) by EUCLID:67; :: thesis: verum