defpred S₁[ Nat] means TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) is second-countable ;
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
Y: ( TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) & TopStruct(# the carrier of (TOP-REAL 1),the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) & TopStruct(# the carrier of (TOP-REAL (n + 1)),the topology of (TOP-REAL (n + 1)) #) = TopSpaceMetr (Euclid (n + 1)) ) by EUCLID:def 8;
n in NAT by ORDINAL1:def 13;
then A2: weight [:TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL 1),the topology of (TOP-REAL 1) #):] = weight TopStruct(# the carrier of (TOP-REAL (n + 1)),the topology of (TOP-REAL (n + 1)) #) by Th4, Y, TOPREAL7:27;
assume S₁[n] ; :: thesis: S₁[n + 1]
then weight [:TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #),TopStruct(# the carrier of (TOP-REAL 1),the topology of (TOP-REAL 1) #):] c= omega by Lm10, WAYBEL23:def 6;
hence S₁[n + 1] by A2, WAYBEL23:def 6; :: thesis: verum

end;

[#] (TOP-REAL 0 ) = REAL 0 by EUCLID:25
.= 0 -tuples_on REAL by EUCLID:def 1
.= {(<*> REAL )} by FINSEQ_2:112 ;
then TopStruct(# the carrier of (TOP-REAL 0 ),the topology of (TOP-REAL 0 ) #) is finite ;
then A3: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1);
hence TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) is second-countable ; :: thesis: verum