let n be Nat; :: thesis: the carrier of (TOP-REAL n) = REAL n
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by Def8;
hence the carrier of (TOP-REAL n) = REAL n ; :: thesis: verum