let F1, F2 be Subset of T; :: according to PRE_TOPC:def 12 :: thesis:
assume that
F1 is closed and
F2 is closed and
A8: F1 misses F2 ; :: thesis:
take F1 ; :: thesis:
take F2 ; :: thesis:
thus ( F1 is open & F2 is open & F1 c= F1 & F2 c= F2 & F1 misses F2 ) by A7, A8; :: thesis:

end;

set TOP = the topology of T;
for A being Subset of T
for U being open Subset of T st A is closed & U is open & A c= U holds
ex W being sequence of (bool the carrier of T) st
( A c= Union W & Union W c= U & ( for n being Element of NAT holds
( Cl (W . n) c= U & W . n is open ) ) )

let A be Subset of T; :: thesis:
let U be open Subset of T; :: thesis:
assume that
A10: A is closed and
U is open and
A11: A c= U ; :: thesis:
defpred S₁[ object , object ] means for p being Point of T st p = c₁ holds
ex W being Subset of T st
( W is open & p in W & Cl W c= U & c₂ = W );
A12: for x being object st x in A holds
ex y being object st
( y in the topology of T & S₁[x,y] )

let x be object ; :: thesis:
assume A13: x in A ; :: thesis:
then reconsider p = x as Point of T ;
U = (U `) ` ;
then consider G1, G2 being Subset of T such that
A14: G1 is open and
A15: G2 is open and
A16: p in G1 and
A17: U ` c= G2 and
A18: G1 misses G2 by A5, A11, A13;
A19: ( Cl (G2 `) = G2 ` & G2 ` c= U ) by A15, A17, PRE_TOPC:22, SUBSET_1:17;
take G1 ; :: thesis:
thus G1 in the topology of T by A14; :: thesis:
G1 c= G2 ` by A18, SUBSET_1:23;
then A20: Cl G1 c= Cl (G2 `) by PRE_TOPC:19;
let q be Point of T; :: thesis:
assume q = x ; :: thesis:
hence ex W being Subset of T st
( W is open & q in W & Cl W c= U & G1 = W ) by A14, A16, A20, A19, XBOOLE_1:1; :: thesis:

end;

consider w being Function of A, the topology of T such that
A21: for x being object st x in A holds
S₁[x,w . x] from FUNCT_2:sch 1(A12);
A ` in the topology of T by A10, PRE_TOPC:def 2;
then ( the topology of T is open & {(A `)} c= the topology of T ) by ZFMISC_1:31;
then reconsider RNG = rng w, AA = {(A `)} as open Subset-Family of T by TOPS_2:11, XBOOLE_1:1;
set RngA = RNG \/ AA;
A22: dom w = A by FUNCT_2:def 1;
[#] T c= union (RNG \/ AA)

then consider W being Subset of T such that
W is open and
A25: x in W and
Cl W c= U and
A26: w . x = W by A21;
W in rng w by A22, A24, A26, FUNCT_1:def 3;
then W in RNG \/ AA by XBOOLE_0:def 3;
hence x in union (RNG \/ AA) by A25, TARSKI:def 4; :: thesis:

end;

end;

end;

G \ AA is countable by A31, CARD_3:95;
then consider W being sequence of (G \ AA) such that
A36: rng W = G \ AA by A35, CARD_3:96;
reconsider W = W as sequence of (bool the carrier of T) by A35, A36, FUNCT_2:6;
take W ; :: thesis:
thus A c= Union W :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in Union W ; :: thesis:
then consider n being Nat such that
A41: x in W . n by PROB_1:12;
A42: n in NAT by ORDINAL1:def 12;
A43: W . n in G \ AA by A36, A40, FUNCT_1:def 3, A42;
then W . n in G by ZFMISC_1:56;
then A44: ( W . n in RNG or W . n in AA ) by A29, XBOOLE_0:def 3;
W . n <> A ` by A43, ZFMISC_1:56;
then consider xx being object such that
A45: ( xx in dom w & w . xx = W . n ) by A44, FUNCT_1:def 3, TARSKI:def 1;
consider W9 being Subset of T such that
W9 is open and
xx in W9 and
A46: Cl W9 c= U and
A47: W . n = W9 by A21, A22, A45;
W9 c= Cl W9 by PRE_TOPC:18;
then x in Cl W9 by A41, A47;
hence x in U by A46; :: thesis:

end;

let n be Element of NAT ; :: thesis:
A48: W . n in G \ AA by A36, A40, FUNCT_1:def 3;
then W . n in G by ZFMISC_1:56;
then A49: ( W . n in RNG or W . n in AA ) by A29, XBOOLE_0:def 3;
W . n <> A ` by A48, ZFMISC_1:56;
then consider xx being object such that
A50: ( xx in dom w & w . xx = W . n ) by A49, FUNCT_1:def 3, TARSKI:def 1;
ex W9 being Subset of T st
( W9 is open & xx in W9 & Cl W9 c= U & W . n = W9 ) by A21, A22, A50;
hence ( Cl (W . n) c= U & W . n is open ) ; :: thesis:

end;

end;