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] )
A2: ( TopStruct(# the carrier of (TOP-REAL (n + 1)), the topology of (TOP-REAL (n + 1)) #) = TopSpaceMetr (Euclid (n + 1)) & n in NAT ) by EUCLID:def 8, ORDINAL1:def 12;
assume S₁[n] ; :: thesis: S₁[n + 1]
then A3: 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 Lm11, WAYBEL23:def 6;
( 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) ) by EUCLID:def 8;
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) #):] = weight TopStruct(# the carrier of (TOP-REAL (n + 1)), the topology of (TOP-REAL (n + 1)) #) by A2, Th4, TOPREAL7:25;
hence S₁[n + 1] by A3, WAYBEL23:def 6; :: thesis: verum

end;

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