TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is T_2 by PCOMPS_1:34;
hence TOP-REAL n is T_2 by Lm2; :: thesis: verum