let T be TopSpace; :: thesis:
assume that
A1: ( T is finite-ind & ind T <= 0 ) and
A2: T is Lindelof ; :: thesis:
set CT = [#] T;
let A, B be closed Subset of T; :: thesis:
assume A3: A misses B ; :: thesis:

suppose A4: [#] T = {} ; :: thesis:

take A ; :: thesis:
take B ; :: thesis:
thus ( A misses B & A \/ B = [#] T & A c= A & B c= B ) by A3, A4; :: thesis:

end;

suppose A5: [#] T <> {} ; :: thesis:

defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & $1 is Point of T & $1 in D2 & $2 is open closed Subset of T & ( D2 c= A ` or D2 c= B ` ) );
A6: for x being object st x in [#] T holds
ex y being object st
( y in bool ([#] T) & S₁[x,y] )

proof

let x be object ; :: thesis:
assume A7: x in [#] T ; :: thesis:
reconsider p = x as Point of T by A7;

per cases ;

suppose p in A ` ; :: thesis:

then consider W being open Subset of T such that
A8: ( p in W & W c= A ` ) and
A9: Fr W is finite-ind and
A10: ind (Fr W) <= 0 - 1 by A1, Th16;
take W ; :: thesis:
thus W in bool ([#] T) ; :: thesis:
take W ; :: thesis:
thus W = W ; :: thesis:
- 1 <= ind (Fr W) by A9, Th5;
then ind (Fr W) = - 1 by A10, XXREAL_0:1;
then Fr W = {} T by A9, Th6;
hence ( x is Point of T & x in W & W is open closed Subset of T & ( W c= A ` or W c= B ` ) ) by A8, TOPGEN_1:14; :: thesis:

end;

suppose A11: not p in A ` ; :: thesis:

A12: A c= B ` by A3, SUBSET_1:23;
p in A by A7, A11, XBOOLE_0:def 5;
then consider W being open Subset of T such that
A13: ( p in W & W c= B ` ) and
A14: Fr W is finite-ind and
A15: ind (Fr W) <= 0 - 1 by A1, A12, Th16;
take W ; :: thesis:
thus W in bool ([#] T) ; :: thesis:
take W ; :: thesis:
- 1 <= ind (Fr W) by A14, Th5;
then ind (Fr W) = - 1 by A15, XXREAL_0:1;
then Fr W = {} T by A14, Th6;
hence ( W = W & x is Point of T & x in W & W is open closed Subset of T & ( W c= A ` or W c= B ` ) ) by A13, TOPGEN_1:14; :: thesis:

end;

consider F being Function of ([#] T),(bool ([#] T)) such that
A16: for x being object st x in [#] T holds
S₁[x,F . x] from FUNCT_2:sch 1(A6);
reconsider RNG = rng F as Subset-Family of T ;
A17: dom F = [#] T by FUNCT_2:def 1;
[#] T c= union RNG

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A18: x in [#] T ; :: thesis:
reconsider p = x as Point of T by A18;
S₁[x,F . x] by A16, A18;
then ( p in F . p & F . p in RNG ) by A17, FUNCT_1:def 3;
hence x in union RNG by TARSKI:def 4; :: thesis:

end;

then [#] T = union RNG ;
then A19: RNG is Cover of T by SETFAM_1:45;
RNG is open

proof

let U be Subset of T; :: according to TOPS_2:def 1 :: thesis:
assume U in RNG ; :: thesis:
then consider x being object such that
A20: ( x in dom F & F . x = U ) by FUNCT_1:def 3;
S₁[x,U] by A20, A16;
hence U is open ; :: thesis:

end;

then consider G being Subset-Family of T such that
A21: G c= RNG and
A22: G is Cover of T and
A23: G is countable by A2, A19, METRIZTS:def 2;
not T is empty by A5;
then A24: not G is empty by A22, TOPS_2:3;
then consider U being sequence of G such that
A25: rng U = G by A23, CARD_3:96;
A26: dom U = NAT by A24, FUNCT_2:def 1;
then reconsider U = U as SetSequence of ([#] T) by A25, FUNCT_2:2;
consider V being SetSequence of ([#] T) such that
A27: union (rng U) = union (rng V) and
A28: for i, j being Nat st i <> j holds
V . i misses V . j and
A29: for n being Nat ex Un being finite Subset-Family of ([#] T) st
( Un = { (U . i) where i is Element of NAT : i < n } & V . n = (U . n) \ (union Un) ) by Th33;
reconsider rngV = rng V as Subset-Family of T ;
set AA = { (V . n) where n is Element of NAT : V . n misses B } ;
A30: { (V . n) where n is Element of NAT : V . n misses B } c= rng V

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (V . n) where n is Element of NAT : V . n misses B } ; :: thesis:
then ( dom V = NAT & ex n being Element of NAT st
( x = V . n & V . n misses B ) ) by FUNCT_2:def 1;
hence x in rng V by FUNCT_1:def 3; :: thesis:

end;

then reconsider AA = { (V . n) where n is Element of NAT : V . n misses B } as Subset-Family of T by XBOOLE_1:1;
set BB = rngV \ AA;
A31: rngV is open

proof

let A be Subset of T; :: according to TOPS_2:def 1 :: thesis:
assume A in rngV ; :: thesis:
then consider m being object such that
A32: m in dom V and
A33: V . m = A by FUNCT_1:def 3;
reconsider m = m as Element of NAT by A32;
consider Un being finite Subset-Family of ([#] T) such that
A34: Un = { (U . i) where i is Element of NAT : i < m } and
A35: V . m = (U . m) \ (union Un) by A29;
reconsider Un = Un as Subset-Family of T ;
U . m in rng U by A26, FUNCT_1:def 3;
then consider x being object such that
A36: ( x in dom F & F . x = U . m ) by A21, A25, FUNCT_1:def 3;
S₁[x,U . m] by A36, A16;
then reconsider UN = U . m as open Subset of T ;
Un is closed

proof

let D be Subset of T; :: according to TOPS_2:def 2 :: thesis:
assume D in Un ; :: thesis:
then ex i being Element of NAT st
( D = U . i & i < m ) by A34;
then D in rng U by A26, FUNCT_1:def 3;
then consider x being object such that
A37: ( x in dom F & F . x = D ) by A21, A25, FUNCT_1:def 3;
S₁[x,D] by A37, A16;
hence D is closed ; :: thesis:

end;

then union Un is closed by TOPS_2:21;
then UN /\ ((union Un) `) is open ;
hence A is open by A33, A35, SUBSET_1:13; :: thesis:

end;

then union AA is open by A30, TOPS_2:11, TOPS_2:19;
then reconsider UAA = union AA, UBB = union (rngV \ AA) as open Subset of T by A31, TOPS_2:15, TOPS_2:19;
A38: UAA misses UBB

proof

assume UAA meets UBB ; :: thesis:
then consider x being object such that
A39: x in union AA and
A40: x in union (rngV \ AA) by XBOOLE_0:3;
consider Ax being set such that
A41: x in Ax and
A42: Ax in AA by A39, TARSKI:def 4;
consider n being Element of NAT such that
A43: V . n = Ax and
A44: V . n misses B by A42;
consider Bx being set such that
A45: x in Bx and
A46: Bx in rngV \ AA by A40, TARSKI:def 4;
Bx in rngV by A46, XBOOLE_0:def 5;
then consider m being object such that
A47: m in dom V and
A48: V . m = Bx by FUNCT_1:def 3;
reconsider m = m as Element of NAT by A47;
not Bx in AA by A46, XBOOLE_0:def 5;
then m <> n by A44, A48;
then V . n misses V . m by A28;
hence contradiction by A41, A43, A45, A48, XBOOLE_0:3; :: thesis:

end;

rngV = (rngV \ AA) \/ AA by A30, XBOOLE_1:45;
then A49: UAA \/ UBB = union G by A25, A27, ZFMISC_1:78
.= [#] T by A22, SETFAM_1:45 ;
then A50: UAA = UBB ` by A38, PRE_TOPC:5;
B misses UAA

proof

assume B meets UAA ; :: thesis:
then consider x being object such that
A51: x in B and
A52: x in union AA by XBOOLE_0:3;
consider Ax being set such that
A53: x in Ax and
A54: Ax in AA by A52, TARSKI:def 4;
ex n being Element of NAT st
( V . n = Ax & V . n misses B ) by A54;
hence contradiction by A51, A53, XBOOLE_0:3; :: thesis:

end;

then A55: B c= UAA ` by SUBSET_1:23;
A misses UBB

proof

assume A meets UBB ; :: thesis:
then consider x being object such that
A56: x in A and
A57: x in union (rngV \ AA) by XBOOLE_0:3;
consider Bx being set such that
A58: x in Bx and
A59: Bx in rngV \ AA by A57, TARSKI:def 4;
Bx in rngV by A59, XBOOLE_0:def 5;
then consider m being object such that
A60: m in dom V and
A61: V . m = Bx by FUNCT_1:def 3;
reconsider m = m as Element of NAT by A60;
not V . m in AA by A59, A61, XBOOLE_0:def 5;
then V . m meets B ;
then consider b being object such that
A62: b in V . m and
A63: b in B by XBOOLE_0:3;
U . m in rng U by A26, FUNCT_1:def 3;
then consider p being object such that
A64: p in dom F and
A65: F . p = U . m by A21, A25, FUNCT_1:def 3;
reconsider Fp = F . p as Subset of T by A65;
A66: ex Un being finite Subset of (bool ([#] T)) st
( Un = { (U . i) where i is Element of NAT : i < m } & V . m = (U . m) \ (union Un) ) by A29;
then b in U . m by A62, XBOOLE_0:def 5;
then Fp meets B by A63, A65, XBOOLE_0:3;
then A67: not Fp c= B ` by SUBSET_1:23;
S₁[p,F . p] by A16, A64;
then A68: U . m c= A ` by A65, A67;
x in U . m by A58, A61, A66, XBOOLE_0:def 5;
hence contradiction by A56, A68, XBOOLE_0:def 5; :: thesis:

end;

then A c= UAA by A50, SUBSET_1:23;
hence ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) by A38, A49, A50, A55; :: thesis:

end;