reconsider R = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:17;
( TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) & TopStruct(# the carrier of (TOP-REAL (1 + 1)), the topology of (TOP-REAL (1 + 1)) #) = TopSpaceMetr (Euclid (1 + 1)) ) by EUCLID:def 8;
then A1: weight [:TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #),TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #):] = weight TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by Th4, TOPREAL7:25;
Cl R = [#] R^1 by BORSUK_5:15;
then R is dense by TOPS_1:def 3;
then R^1 is separable by TOPGEN_4:6;
then A2: weight [:R^1,R^1:] c= omega by TOPMETR:def 6, WAYBEL23:def 6;
TopStruct(# the carrier of [:R^1,R^1:], the topology of [:R^1,R^1:] #), TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) are_homeomorphic by TOPREAL6:77, TOPREALA:15;
then A3: weight TopStruct(# the carrier of [:R^1,R^1:], the topology of [:R^1,R^1:] #) = weight TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) by Th4;
weight TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) c= weight [:TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #),TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #):] by Th6;
then weight TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) c= omega by A1, A3, A2;
hence TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) is second-countable by WAYBEL23:def 6; :: thesis: verum