TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
hence TOP-REAL n is first-countable by Th35; :: thesis: verum