let T be non empty TopSpace; :: thesis:
let F be Subset-Family of T; :: thesis:
let S be SetSequence of T; :: thesis:
assume that
A1: rng S c= F and
A2: S is non-empty ; :: thesis:
defpred S₁[ object , object ] means for i being Nat st i = $1 holds
ex SS being Subset-Family of T st
( SS c= F & SS = { (S . j) where j is Element of NAT : j >= i } & $2 = Cl (union SS) );
A3: for x being object st x in NAT holds
ex y being object st
( y in bool the carrier of T & S₁[x,y] )

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider x9 = x as Nat ;
set SS = { (S . j) where j is Element of NAT : j >= x9 } ;
{ (S . j) where j is Element of NAT : j >= x9 } c= bool the carrier of T

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in { (S . j) where j is Element of NAT : j >= x9 } ; :: thesis:
then ex j being Element of NAT st
( S . j = y & j >= x9 ) ;
hence y in bool the carrier of T ; :: thesis:

end;

then reconsider SS = { (S . j) where j is Element of NAT : j >= x9 } as Subset-Family of T ;
take Cl (union SS) ; :: thesis:
SS c= F

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in SS ; :: thesis:
then consider j being Element of NAT such that
A4: ( S . j = y & j >= x9 ) ;
dom S = NAT by FUNCT_2:def 1;
then y in rng S by A4, FUNCT_1:def 3;
hence y in F by A1; :: thesis:

end;

hence ( Cl (union SS) in bool the carrier of T & S₁[x, Cl (union SS)] ) ; :: thesis:

end;

consider R being SetSequence of T such that
A5: for x being object st x in NAT holds
S₁[x,R . x] from FUNCT_2:sch 1(A3);

let n be object ; :: thesis:
assume n in dom R ; :: thesis:
then reconsider n9 = n as Element of NAT ;
A7: S . n9 c= Cl (S . n9) by PRE_TOPC:18;
consider SS being Subset-Family of T such that
SS c= F and
A8: SS = { (S . j) where j is Element of NAT : j >= n9 } and
A9: R . n9 = Cl (union SS) by A5;
S . n9 in SS by A8;
then A10: Cl (S . n9) c= Cl (union SS) by PRE_TOPC:19, ZFMISC_1:74;
dom S = NAT by FUNCT_2:def 1;
hence not R . n is empty by A2, A9, A7, A10, FUNCT_1:def 9; :: thesis:

end;

let n be Nat; :: thesis:
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
ex SS being Subset-Family of T st
( SS c= F & SS = { (S . j) where j is Element of NAT : j >= n9 } & R . n9 = Cl (union SS) ) by A5;
hence R . n is closed ; :: thesis:

end;

then reconsider R = R as non-empty closed SetSequence of T by A6, Def6, FUNCT_1:def 9;
take R ; :: thesis:

let n be Nat; :: thesis:
A11: n in NAT by ORDINAL1:def 12;
consider Sn being Subset-Family of T such that
Sn c= F and
A12: Sn = { (S . j) where j is Element of NAT : j >= n } and
A13: R . n = Cl (union Sn) by A5, A11;
consider Sn1 being Subset-Family of T such that
Sn1 c= F and
A14: Sn1 = { (S . j) where j is Element of NAT : j >= n + 1 } and
A15: R . (n + 1) = Cl (union Sn1) by A5;
Sn1 c= Sn

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in Sn1 ; :: thesis:
then consider j being Element of NAT such that
A16: y = S . j and
A17: j >= n + 1 by A14;
j >= n by A17, NAT_1:13;
hence y in Sn by A12, A16; :: thesis:

end;

end;

A18: dom S = NAT by FUNCT_2:def 1;
then reconsider rngS = rng S as non empty Subset-Family of T by RELAT_1:42;
reconsider Sp = S as sequence of rngS by A18, FUNCT_2:1;
assume that
A19: F is locally_finite and
A20: S is one-to-one ; :: thesis:
reconsider S9 = Sp " as Function ;
reconsider S9 = S9 as Function of rngS,NAT by A20, FUNCT_2:25;
deffunc H₁( Element of rngS) -> Element of NAT = S9 . $1;
assume meet R <> {} ; :: thesis:
then consider x being object such that
A21: x in meet R by XBOOLE_0:def 1;
reconsider x = x as Point of T by A21;
rng S is locally_finite by A1, A19, PCOMPS_1:9;
then consider W being Subset of T such that
A22: x in W and
A23: W is open and
A24: { V where V is Subset of T : ( V in rngS & V meets W ) } is finite ;
set X = { V where V is Subset of T : ( V in rngS & V meets W ) } ;
set Y = { H₁(z) where z is Element of rngS : z in { V where V is Subset of T : ( V in rngS & V meets W ) } } ;
A25: { H₁(z) where z is Element of rngS : z in { V where V is Subset of T : ( V in rngS & V meets W ) } } is finite from FRAENKEL:sch 21(A24);
{ H₁(z) where z is Element of rngS : z in { V where V is Subset of T : ( V in rngS & V meets W ) } } c= NAT

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in { H₁(z) where z is Element of rngS : z in { V where V is Subset of T : ( V in rngS & V meets W ) } } ; :: thesis:
then ex z being Element of rngS st
( y = H₁(z) & z in { V where V is Subset of T : ( V in rngS & V meets W ) } ) ;
hence y in NAT ; :: thesis:

end;

then reconsider Y = { H₁(z) where z is Element of rngS : z in { V where V is Subset of T : ( V in rngS & V meets W ) } } as Subset of NAT ;
consider n being Nat such that
A26: for k being Nat st k in Y holds
k <= n by A25, STIRL2_1:56;
set n1 = n + 1;
A27: x in R . (n + 1) by A21, KURATO_0:3;
consider Sn being Subset-Family of T such that
A28: Sn c= F and
A29: Sn = { (S . j) where j is Element of NAT : j >= n + 1 } and
A30: R . (n + 1) = Cl (union Sn) by A5;
Cl (union Sn) = union (clf Sn) by A19, A28, PCOMPS_1:9, PCOMPS_1:20;
then consider CLF being set such that
A31: x in CLF and
A32: CLF in clf Sn by A30, A27, TARSKI:def 4;
reconsider CLF = CLF as Subset of T by A32;
consider U being Subset of T such that
A33: CLF = Cl U and
A34: U in Sn by A32, PCOMPS_1:def 2;
consider j being Element of NAT such that
A35: U = S . j and
A36: j >= n + 1 by A29, A34;
A37: Sp . j in rngS ;
Sp . j meets W by A22, A23, A31, A33, A35, TOPS_1:12;
then A38: Sp . j in { V where V is Subset of T : ( V in rngS & V meets W ) } by A37;
(S ") . (S . j) = j by A20, FUNCT_2:26;
then j in Y by A38;
then j <= n by A26;
hence contradiction by A36, NAT_1:13; :: thesis:

end;

let i be Nat; :: thesis:
i in NAT by ORDINAL1:def 12;
then ex SS being Subset-Family of T st
( SS c= F & SS = { (S . j) where j is Element of NAT : j >= i } & R . i = Cl (union SS) ) by A5;
hence ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } ) ; :: thesis: