set T = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #);
A1: for x being set holds
( x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } iff x in { (card B) where B is Basis of (TOP-REAL n) : verum } )

proof

let x be set ; :: thesis: ( x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } iff x in { (card B) where B is Basis of (TOP-REAL n) : verum } )

hereby :: thesis: ( x in { (card B) where B is Basis of (TOP-REAL n) : verum } implies x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } )

assume x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } ; :: thesis: x in { (card B) where B is Basis of (TOP-REAL n) : verum }
then consider B1 being Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) such that
A2: x = card B1 ;
reconsider B2 = B1 as Basis of (TOP-REAL n) by YELLOW12:32;
x = card B2 by A2;
hence x in { (card B) where B is Basis of (TOP-REAL n) : verum } ; :: thesis: verum

end;

assume x in { (card B) where B is Basis of (TOP-REAL n) : verum } ; :: thesis: x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum }
then consider B1 being Basis of (TOP-REAL n) such that
A3: x = card B1 ;
reconsider B2 = B1 as Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by YELLOW12:32;
x = card B2 by A3;
hence x in { (card B) where B is Basis of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) : verum } ; :: thesis: verum

end;

weight TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = weight (TOP-REAL n) by A1, TARSKI:1;
then weight (TOP-REAL n) c= omega by WAYBEL23:def 6;
hence TOP-REAL n is second-countable by WAYBEL23:def 6; :: thesis: verum