set TR = TOP-REAL n;
set T = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #);
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = (TOP-REAL n) | ([#] (TOP-REAL n)) by TSEP_1:93;
then weight TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = weight (TOP-REAL n) by Th1, METRIZTS:4;
hence TOP-REAL n is second-countable by WAYBEL23:def 6; :: thesis: verum