let n be Nat; :: thesis: for T being TopSpace
for g being SetSequence of T st ( for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) holds
ex G being Subset-Family of T st
( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G )
let T be TopSpace; :: thesis: for g being SetSequence of T st ( for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) holds
ex G being Subset-Family of T st
( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G )
let g be SetSequence of T; :: thesis: ( ( for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) implies ex G being Subset-Family of T st
( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G ) )
assume A1: for i being Nat holds
( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ; :: thesis: ex G being Subset-Family of T st
( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G )
defpred S₁[ object , object ] means for n being Nat
for F being Subset-Family of T st n = $1 & F = $2 holds
( union F = g . n & F is closed & F is countable );
A2: for x being object st x in NAT holds
ex y being object st
( y in bool (bool the carrier of T) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in bool (bool the carrier of T) & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in bool (bool the carrier of T) & S₁[x,y] )
then reconsider n = x as Element of NAT ;
g . n is F_sigma by A1;
then consider y being closed countable Subset-Family of T such that
A3: g . n = union y by TOPGEN_4:def 6;
take y ; :: thesis: ( y in bool (bool the carrier of T) & S₁[x,y] )
thus ( y in bool (bool the carrier of T) & S₁[x,y] ) by A3; :: thesis: verum

end;

consider f being SetSequence of (bool the carrier of T) such that
A4: for x being object st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
take F = Union f; :: thesis: ( F is closed & F is finite-ind & ind F <= n & F is countable & Union g = union F )
thus F is closed :: thesis: ( F is finite-ind & ind F <= n & F is countable & Union g = union F )

proof

let A be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not A in F or A is closed )
assume A in F ; :: thesis: A is closed
then consider n being Nat such that
A5: A in f . n by PROB_1:12;
n in NAT by ORDINAL1:def 12;
then f . n is closed by A4;
hence A is closed by A5; :: thesis: verum

end;

for A being Subset of T st A in F holds
( A is finite-ind & ind A <= n )

proof

let A be Subset of T; :: thesis: ( A in F implies ( A is finite-ind & ind A <= n ) )
assume A in F ; :: thesis: ( A is finite-ind & ind A <= n )
then consider i being Nat such that
A6: A in f . i by PROB_1:12;
i in NAT by ORDINAL1:def 12;
then union (f . i) = g . i by A4;
then A7: A c= g . i by A6, ZFMISC_1:74;
A8: ind (g . i) <= n by A1;
A9: g . i is finite-ind by A1;
then ind A <= ind (g . i) by A7, TOPDIM_1:19;
hence ( A is finite-ind & ind A <= n ) by A7, A8, A9, TOPDIM_1:19, XXREAL_0:2; :: thesis: verum

end;

hence ( F is finite-ind & ind F <= n ) by TOPDIM_1:11; :: thesis: ( F is countable & Union g = union F )
for x being set st x in dom f holds
f . x is countable by A4;
hence F is countable by CARD_4:11; :: thesis: Union g = union F
thus Union g c= union F :: according to XBOOLE_0:def 10 :: thesis: union F c= Union g

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Union g or x in union F )
assume x in Union g ; :: thesis: x in union F
then consider i being Nat such that
A10: x in g . i by PROB_1:12;
i in NAT by ORDINAL1:def 12;
then union (f . i) = g . i by A4;
then consider y being set such that
A11: x in y and
A12: y in f . i by A10, TARSKI:def 4;
y in F by A12, PROB_1:12;
hence x in union F by A11, TARSKI:def 4; :: thesis: verum

end;

thus union F c= Union g :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union F or x in Union g )
assume x in union F ; :: thesis: x in Union g
then consider y being set such that
A13: x in y and
A14: y in F by TARSKI:def 4;
consider i being Nat such that
A15: y in f . i by A14, PROB_1:12;
i in NAT by ORDINAL1:def 12;
then union (f . i) = g . i by A4;
then x in g . i by A13, A15, TARSKI:def 4;
hence x in Union g by PROB_1:12; :: thesis: verum

end;