reconsider R = RAT as Subset of R^1 by NUMBERS:12, TOPMETR:24;
( 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:27;
Cl R = [#] R^1 by BORSUK_5:35;
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 7, 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:86, TOPREALA:36;
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, XBOOLE_1:1;
hence TopStruct(# the carrier of (TOP-REAL 1),the topology of (TOP-REAL 1) #) is second-countable by WAYBEL23:def 6; :: thesis: verum