let T be TopSpace; :: thesis:
assume that
A1: T is T_4 and
A2: T is Lindelof ; :: thesis:
set CT = [#] T;
given F being Subset-Family of T such that A3: F is closed and
A4: F is Cover of T and
A5: F is countable and
A6: ( F is finite-ind & ind F <= 0 ) ; :: thesis:

suppose union F is empty ; :: thesis:

then [#] T = {} T by A4, SETFAM_1:45;
hence ( T is finite-ind & ind T <= 0 ) by Th6; :: thesis:

end;

suppose A7: not union F is empty ; :: thesis:

then reconsider CT = [#] T as non empty set ;
consider f being sequence of F such that
A8: F = rng f by A5, A7, CARD_3:96, ZFMISC_1:2;
A9: dom f = NAT by A7, FUNCT_2:def 1, ZFMISC_1:2;

now :: thesis:

set CTT = [:(bool CT),(bool CT):];
defpred S₁[ object , object ] means for n being Nat
for A, B being Subset of T st $1 = [n,[A,B]] holds
( ( Cl A meets Cl B implies $2 = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & $2 = [G,H] & Cl G misses Cl H ) ) );
set TOP = the topology of T;
let A, B be closed Subset of T; :: thesis:
assume A10: A misses B ; :: thesis:
A11: ( Cl A = A & Cl B = B ) by PRE_TOPC:22;
A12: for x being object st x in [:NAT,[:(bool CT),(bool CT):]:] holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis:
assume x in [:NAT,[:(bool CT),(bool CT):]:] ; :: thesis:
then consider n9, ab being object such that
A13: n9 in NAT and
A14: ab in [:(bool CT),(bool CT):] and
A15: x = [n9,ab] by ZFMISC_1:def 2;
consider A9, B9 being object such that
A16: ( A9 in bool CT & B9 in bool CT ) and
A17: ab = [A9,B9] by A14, ZFMISC_1:def 2;
reconsider A9 = A9, B9 = B9 as Subset of T by A16;

per cases ;

suppose A18: Cl A9 meets Cl B9 ; :: thesis:

take ab ; :: thesis:
let n be Nat; :: thesis:
let A, B be Subset of T; :: thesis:
assume x = [n,[A,B]] ; :: thesis:
then A19: ab = [A,B] by A15, XTUPLE_0:1;
then A = A9 by A17, XTUPLE_0:1;
hence ( ( Cl A meets Cl B implies ab = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & ab = [G,H] & Cl G misses Cl H ) ) ) by A17, A18, A19, XTUPLE_0:1; :: thesis:

end;

suppose A20: Cl A9 misses Cl B9 ; :: thesis:

A21: f . n9 in rng f by A9, A13, FUNCT_1:def 3;
then reconsider fn = f . n9 as Subset of T by A8;
A22: fn is closed by A3, A21;
A23: fn is finite-ind by A6, A21, Th11;
then A24: ind (T | fn) = ind fn by Lm5;
A25: ind fn <= 0 by A6, A21, Th11;
A26: [#] (T | fn) = fn by PRE_TOPC:def 5;
then reconsider Af = (Cl A9) /\ fn, Bf = (Cl B9) /\ fn as Subset of (T | fn) by XBOOLE_1:17;
A27: ( Af is closed & Bf is closed ) by A26, PRE_TOPC:13;
Af misses Bf by A20, XBOOLE_1:76;
then consider AF, BF being closed Subset of (T | fn) such that
A28: AF misses BF and
A29: AF \/ BF = [#] (T | fn) and
A30: Af c= AF and
A31: Bf c= BF by A2, A22, A25, A23, A24, A27, Th34;
[#] (T | fn) c= [#] T by PRE_TOPC:def 4;
then reconsider af = AF, bf = BF as Subset of T by XBOOLE_1:1;
A32: af \/ (Cl A9) misses bf \/ (Cl B9)

proof

assume af \/ (Cl A9) meets bf \/ (Cl B9) ; :: thesis:
then consider x being object such that
A33: ( x in af \/ (Cl A9) & x in bf \/ (Cl B9) ) by XBOOLE_0:3;

per cases by A33, XBOOLE_0:def 3;

suppose ( ( x in af & x in bf ) or ( x in Cl A9 & x in Cl B9 ) ) ; :: thesis:

hence contradiction by A20, A28, XBOOLE_0:3; :: thesis:

end;

suppose A34: ( x in af & x in Cl B9 ) ; :: thesis:

then x in Bf by A26, XBOOLE_0:def 4;
hence contradiction by A28, A31, A34, XBOOLE_0:3; :: thesis:

end;

suppose A35: ( x in bf & x in Cl A9 ) ; :: thesis:

then x in Af by A26, XBOOLE_0:def 4;
hence contradiction by A28, A30, A35, XBOOLE_0:3; :: thesis:

end;

( bf is closed & af is closed ) by A22, A26, TSEP_1:8;
then consider U, W being open Subset of T such that
A36: af \/ (Cl A9) c= U and
A37: bf \/ (Cl B9) c= W and
A38: Cl U misses Cl W by A1, A32, Th2;
take uw = [U,W]; :: thesis:
let n be Nat; :: thesis:
let A, B be Subset of T; :: thesis:
assume A39: x = [n,[A,B]] ; :: thesis:
then A40: n = n9 by A15, XTUPLE_0:1;
A41: ab = [A,B] by A15, A39, XTUPLE_0:1;
then B = B9 by A17, XTUPLE_0:1;
then A42: Cl B c= W by A37, XBOOLE_1:11;
( af c= U & bf c= W ) by A36, A37, XBOOLE_1:11;
then A43: f . n c= U \/ W by A26, A29, A40, XBOOLE_1:13;
A44: A = A9 by A17, A41, XTUPLE_0:1;
then Cl A c= U by A36, XBOOLE_1:11;
hence ( ( Cl A meets Cl B implies uw = [A,B] ) & ( Cl A misses Cl B implies ex G, H being open Subset of T st
( f . n c= G \/ H & Cl A c= G & Cl B c= H & uw = [G,H] & Cl G misses Cl H ) ) ) by A17, A20, A38, A41, A42, A43, A44, XTUPLE_0:1; :: thesis:

end;

consider GH being Function such that
dom GH = [:NAT,[:(bool CT),(bool CT):]:] and
A45: for x being object st x in [:NAT,[:(bool CT),(bool CT):]:] holds
S₁[x,GH . x] from CLASSES1:sch 1(A12);
deffunc H₁( set , set ) -> set = GH . [$1,$2];
consider ghSeq being Function such that
A46: dom ghSeq = NAT and
A47: ghSeq . 0 = [A,B] and
A48: for n being Nat holds ghSeq . (n + 1) = H₁(n,ghSeq . n) from NAT_1:sch 11();
defpred S₂[ Nat] means ( ghSeq . $1 in [:(bool CT),(bool CT):] & ( for A, B being Subset of T st A = (ghSeq . $1) `1 & B = (ghSeq . $1) `2 holds
Cl A misses Cl B ) );
A49: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume A50: S₂[n] ; :: thesis:
consider A, B being object such that
A51: ( A in bool CT & B in bool CT ) and
A52: ghSeq . n = [A,B] by A50, ZFMISC_1:def 2;
reconsider A = A, B = B as Subset of T by A51;
n in NAT by ORDINAL1:def 12;
then A53: [n,(ghSeq . n)] in [:NAT,[:(bool CT),(bool CT):]:] by A50, ZFMISC_1:87;
Cl A misses Cl B by A50, A52;
then consider G, H being open Subset of T such that
f . n c= G \/ H and
Cl A c= G and
Cl B c= H and
A54: GH . [n,(ghSeq . n)] = [G,H] and
A55: Cl G misses Cl H by A45, A52, A53;
A56: ghSeq . (n + 1) = [G,H] by A48, A54;
thus S₂[n + 1] by A55, A56; :: thesis:

end;

A57: S₂[ 0 ] by A10, A11, A47;
A58: for n being Nat holds S₂[n] from NAT_1:sch 2(A57, A49);
rng ghSeq c= [:(bool CT),(bool CT):]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ghSeq ; :: thesis:
then ex x being object st
( x in dom ghSeq & ghSeq . x = y ) by FUNCT_1:def 3;
hence y in [:(bool CT),(bool CT):] by A46, A58; :: thesis:

end;

then reconsider ghSeq = ghSeq as sequence of [:(bool CT),(bool CT):] by A46, FUNCT_2:2;
set g = pr1 ghSeq;
set h = pr2 ghSeq;
A59: (pr2 ghSeq) . 0 = [A,B] `2 by A47, FUNCT_2:def 6
.= B ;
reconsider RngH = rng ((pr2 ghSeq) ^\ 1), RngG = rng ((pr1 ghSeq) ^\ 1) as Subset-Family of T ;
A60: (pr1 ghSeq) . 0 = [A,B] `1 by A47, FUNCT_2:def 5
.= A ;
A61: for n being Nat holds
( (pr1 ghSeq) . (n + 1) in the topology of T & (pr2 ghSeq) . (n + 1) in the topology of T & (pr1 ghSeq) . n c= (pr1 ghSeq) . (n + 1) & (pr2 ghSeq) . n c= (pr2 ghSeq) . (n + 1) & (pr1 ghSeq) . n misses (pr2 ghSeq) . n & f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1)) )

proof

let n be Nat; :: thesis:
consider A, B being object such that
A62: ( A in bool CT & B in bool CT ) and
A63: ghSeq . n = [A,B] by ZFMISC_1:def 2;
reconsider A = A, B = B as Subset of T by A62;
A64: n in NAT by ORDINAL1:def 12;
then A65: [n,(ghSeq . n)] in [:NAT,[:(bool CT),(bool CT):]:] by ZFMISC_1:87;
A66: A = [A,B] `1 ;
then A67: A = (pr1 ghSeq) . n by A46, A64, A63, MCART_1:def 12;
A68: B = [A,B] `2 ;
then A69: B = (pr2 ghSeq) . n by A46, A64, A63, MCART_1:def 13;
Cl A misses Cl B by A58, A66, A68, A63;
then consider G, H being open Subset of T such that
A70: f . n c= G \/ H and
A71: Cl A c= G and
A72: Cl B c= H and
A73: GH . [n,(ghSeq . n)] = [G,H] and
Cl G misses Cl H by A45, A63, A65;
A74: ghSeq . (n + 1) = [G,H] by A48, A73;
A75: G = [G,H] `1
.= (pr1 ghSeq) . (n + 1) by A46, A74, MCART_1:def 12 ;
hence (pr1 ghSeq) . (n + 1) in the topology of T by PRE_TOPC:def 2; :: thesis:
A76: H = [G,H] `2
.= (pr2 ghSeq) . (n + 1) by A46, A74, MCART_1:def 13 ;
hence (pr2 ghSeq) . (n + 1) in the topology of T by PRE_TOPC:def 2; :: thesis:
A c= Cl A by PRE_TOPC:18;
hence (pr1 ghSeq) . n c= (pr1 ghSeq) . (n + 1) by A67, A71, A75; :: thesis:
B c= Cl B by PRE_TOPC:18;
hence (pr2 ghSeq) . n c= (pr2 ghSeq) . (n + 1) by A69, A72, A76; :: thesis:
( A c= Cl A & B c= Cl B ) by PRE_TOPC:18;
hence (pr1 ghSeq) . n misses (pr2 ghSeq) . n by A58, A66, A67, A68, A69, A63, XBOOLE_1:64; :: thesis:
thus f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1)) by A70, A75, A76; :: thesis:

end;

then for n being Nat holds (pr1 ghSeq) . n c= (pr1 ghSeq) . (n + 1) ;
then A77: pr1 ghSeq is non-descending by KURATO_0:def 4;
A78: RngH is open

proof

A79: RngH = { ((pr2 ghSeq) . n) where n is Nat : n >= 1 } by SETLIM_1:6;
let A be Subset of T; :: according to TOPS_2:def 1 :: thesis:
assume A in RngH ; :: thesis:
then consider n being Nat such that
A80: (pr2 ghSeq) . n = A and
A81: n >= 1 by A79;
reconsider n1 = n - 1 as Nat by A81, NAT_1:21;
(pr2 ghSeq) . (n1 + 1) in the topology of T by A61;
hence A is open by A80, PRE_TOPC:def 2; :: thesis:

end;

RngG is open

proof

A82: RngG = { ((pr1 ghSeq) . n) where n is Nat : n >= 1 } by SETLIM_1:6;
let A be Subset of T; :: according to TOPS_2:def 1 :: thesis:
assume A in RngG ; :: thesis:
then consider n being Nat such that
A83: (pr1 ghSeq) . n = A and
A84: n >= 1 by A82;
reconsider n1 = n - 1 as Nat by A84, NAT_1:21;
(pr1 ghSeq) . (n1 + 1) in the topology of T by A61;
hence A is open by A83, PRE_TOPC:def 2; :: thesis:

end;

then reconsider unionG = union RngG, unionH = union RngH as open Subset of T by A78, TOPS_2:19;
for n being Nat holds (pr2 ghSeq) . n c= (pr2 ghSeq) . (n + 1) by A61;
then A85: pr2 ghSeq is non-descending by KURATO_0:def 4;
A86: unionH misses unionG

proof

assume unionH meets unionG ; :: thesis:
then consider x being object such that
A87: x in unionH and
A88: x in unionG by XBOOLE_0:3;
consider H being set such that
A89: x in H and
A90: H in RngH by A87, TARSKI:def 4;
RngH = { ((pr2 ghSeq) . n) where n is Nat : n >= 1 } by SETLIM_1:6;
then consider i being Nat such that
A91: (pr2 ghSeq) . i = H and
i >= 1 by A90;
consider G being set such that
A92: x in G and
A93: G in RngG by A88, TARSKI:def 4;
RngG = { ((pr1 ghSeq) . n) where n is Nat : n >= 1 } by SETLIM_1:6;
then consider j being Nat such that
A94: (pr1 ghSeq) . j = G and
j >= 1 by A93;

per cases ;

suppose A95: i <= j ; :: thesis:

A96: (pr1 ghSeq) . j misses (pr2 ghSeq) . j by A61;
(pr2 ghSeq) . i c= (pr2 ghSeq) . j by A85, A95, PROB_1:def 5;
hence contradiction by A92, A94, A89, A91, A96, XBOOLE_0:3; :: thesis:

end;

suppose A97: i >= j ; :: thesis:

A98: (pr1 ghSeq) . i misses (pr2 ghSeq) . i by A61;
(pr1 ghSeq) . j c= (pr1 ghSeq) . i by A77, A97, PROB_1:def 5;
hence contradiction by A92, A94, A89, A91, A98, XBOOLE_0:3; :: thesis:

end;

A99: CT c= unionH \/ unionG

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in CT ; :: thesis:
then reconsider x = x as Point of T ;
union F = CT by A4, SETFAM_1:45;
then consider X being set such that
A100: x in X and
A101: X in rng f by A8, TARSKI:def 4;
consider n being object such that
A102: n in dom f and
A103: f . n = X by A101, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A102;
A104: n + 1 >= 1 by NAT_1:12;
A105: f . n c= ((pr1 ghSeq) . (n + 1)) \/ ((pr2 ghSeq) . (n + 1)) by A61;

per cases by A100, A103, A105, XBOOLE_0:def 3;

suppose A106: x in (pr1 ghSeq) . (n + 1) ; :: thesis:

RngG = { ((pr1 ghSeq) . i) where i is Nat : i >= 1 } by SETLIM_1:6;
then (pr1 ghSeq) . (n + 1) in RngG by A104;
then x in unionG by A106, TARSKI:def 4;
hence x in unionH \/ unionG by XBOOLE_0:def 3; :: thesis:

end;

suppose A107: x in (pr2 ghSeq) . (n + 1) ; :: thesis:

RngH = { ((pr2 ghSeq) . i) where i is Nat : i >= 1 } by SETLIM_1:6;
then (pr2 ghSeq) . (n + 1) in RngH by A104;
then x in unionH by A107, TARSKI:def 4;
hence x in unionH \/ unionG by XBOOLE_0:def 3; :: thesis:

end;

then CT = unionH \/ unionG ;
then ( unionH = unionG ` & unionG = unionH ` ) by A86, PRE_TOPC:5;
then reconsider unionG = unionG, unionH = unionH as closed Subset of T ;
take unionG = unionG; :: thesis:
take unionH = unionH; :: thesis:
thus unionG misses unionH by A86; :: thesis:
thus unionG \/ unionH = [#] T by A99; :: thesis:
RngG = { ((pr1 ghSeq) . i) where i is Nat : i >= 1 } by SETLIM_1:6;
then (pr1 ghSeq) . 1 in RngG ;
then A108: (pr1 ghSeq) . 1 c= unionG by ZFMISC_1:74;
(pr1 ghSeq) . 0 c= (pr1 ghSeq) . (0 + 1) by A61;
hence A c= unionG by A108, A60; :: thesis:
RngH = { ((pr2 ghSeq) . i) where i is Nat : i >= 1 } by SETLIM_1:6;
then (pr2 ghSeq) . 1 in RngH ;
then A109: (pr2 ghSeq) . 1 c= unionH by ZFMISC_1:74;
(pr2 ghSeq) . 0 c= (pr2 ghSeq) . (0 + 1) by A61;
hence B c= unionH by A109, A59; :: thesis:

end;

hence ( T is finite-ind & ind T <= 0 ) by A1, Th32; :: thesis:

end;