let T be TopSpace; :: thesis:
assume that
A5: T is regular and
A6: T is Lindelof ; :: thesis:

suppose A7: T is empty ; :: thesis:

let F1, F2 be Subset of T; :: according to PRE_TOPC:def 18 :: 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;

suppose A9: not T is empty ; :: thesis:

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 Function of NAT ,(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₁[ set , set ] 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 set st x in A holds
ex y being set st
( y in the topology of T & S₁[x,y] )

let x be set ; :: 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, PRE_TOPC:def 17;
take G1 ; :: thesis:
thus G1 in the topology of T by A14, PRE_TOPC:def 5; :: thesis:
G1 c= G2 ` by A18, SUBSET_1:43;
then A20: Cl G1 c= Cl (G2 ` ) by PRE_TOPC:49;
let q be Point of T; :: thesis:
assume A21: q = x ; :: thesis:
( Cl (G2 ` ) = G2 ` & G2 ` c= U ) by A15, A17, PRE_TOPC:52, SUBSET_1:36;
hence ex W being Subset of T st
( W is open & q in W & Cl W c= U & G1 = W ) by A14, A16, A20, A21, XBOOLE_1:1; :: thesis:

end;

consider w being Function of A,the topology of T such that
A22: for x being set 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 5;
then ( the topology of T is open & {(A ` )} c= the topology of T ) by CANTOR_1:3, ZFMISC_1:37;
then reconsider RNG = rng w, AA = {(A ` )} as open Subset-Family of T by TOPS_2:18, XBOOLE_1:1;
set RngA = RNG \/ AA;
A23: dom w = A by FUNCT_2:def 1;
[#] T c= union (RNG \/ AA)

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A24: x in [#] T ; :: thesis:
then reconsider p = x as Point of T ;

per cases ;

suppose A25: x in A ; :: thesis:

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

end;

suppose A28: not x in A ; :: thesis:

A ` in AA by TARSKI:def 1;
then A29: A ` in RNG \/ AA by XBOOLE_0:def 3;
x in A ` by A24, A28, XBOOLE_0:def 5;
hence x in union (RNG \/ AA) by A29, TARSKI:def 4; :: thesis:

end;

then ( RNG \/ AA is open Subset-Family of T & RNG \/ AA is Cover of T ) by SETFAM_1:def 12, TOPS_2:20;
then consider G being Subset-Family of T such that
A30: G c= RNG \/ AA and
A31: G is Cover of T and
A32: G is countable by A6, Def2;
A33: [#] T = union G by A31, SETFAM_1:60;

per cases ;

suppose G \ AA is empty ; :: thesis:

then G c= AA by XBOOLE_1:37;
then A34: union G c= union AA by ZFMISC_1:95;
take W = NAT --> ({} T); :: thesis:
rng W = {({} T)} by FUNCOP_1:14;
then A35: ( ({} T) ` = [#] T & Union W = {} T ) by ZFMISC_1:31;
union AA = A ` by ZFMISC_1:31;
then A ` = [#] T by A33, A34, XBOOLE_0:def 10;
hence ( A c= Union W & Union W c= U ) by A35, SUBSET_1:64, XBOOLE_1:2; :: thesis:
let n be Element of NAT ; :: thesis:
W . n = {} T by FUNCOP_1:13;
then Cl (W . n) = {} T by PRE_TOPC:52;
hence ( Cl (W . n) c= U & W . n is open ) by FUNCOP_1:13, XBOOLE_1:2; :: thesis:

end;

suppose A36: not G \ AA is empty ; :: thesis:

G \ AA is countable by A32, CARD_3:130;
then consider W being Function of NAT ,(G \ AA) such that
A37: rng W = G \ AA by A36, CARD_3:146;
reconsider W = W as Function of NAT ,(bool the carrier of T) by A36, A37, FUNCT_2:8;
take W ; :: thesis:
thus A c= Union W :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A38: x in A ; :: thesis:
then consider y being set such that
A39: x in y and
A40: y in G by A33, TARSKI:def 4;
not x in A ` by A38, XBOOLE_0:def 5;
then not y in AA by A39, TARSKI:def 1;
then y in rng W by A37, A40, XBOOLE_0:def 5;
then ex n being set st
( n in dom W & W . n = y ) by FUNCT_1:def 5;
hence x in Union W by A39, PROB_1:25; :: thesis:

end;

A41: dom W = NAT by FUNCT_2:def 1;
thus Union W c= U :: thesis:

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in Union W ; :: thesis:
then consider n being Element of NAT such that
A42: x in W . n by PROB_1:25;
A43: W . n in G \ AA by A37, A41, FUNCT_1:def 5;
then W . n in G by ZFMISC_1:64;
then A44: ( W . n in RNG or W . n in AA ) by A30, XBOOLE_0:def 3;
W . n <> A ` by A43, ZFMISC_1:64;
then consider xx being set such that
A45: ( xx in dom w & w . xx = W . n ) by A44, FUNCT_1:def 5, TARSKI:def 1;
consider W' being Subset of T such that
W' is open and
xx in W' and
A46: Cl W' c= U and
A47: W . n = W' by A22, A23, A45;
W' c= Cl W' by PRE_TOPC:48;
then x in Cl W' by A42, A47;
hence x in U by A46; :: thesis:

end;

let n be Element of NAT ; :: thesis:
A48: W . n in G \ AA by A37, A41, FUNCT_1:def 5;
then W . n in G by ZFMISC_1:64;
then A49: ( W . n in RNG or W . n in AA ) by A30, XBOOLE_0:def 3;
W . n <> A ` by A48, ZFMISC_1:64;
then consider xx being set such that
A50: ( xx in dom w & w . xx = W . n ) by A49, FUNCT_1:def 5, TARSKI:def 1;
ex W' being Subset of T st
( W' is open & xx in W' & Cl W' c= U & W . n = W' ) by A22, A23, A50;
hence ( Cl (W . n) c= U & W . n is open ) ; :: thesis:

end;

hence T is normal by A9, NAGATA_1:18; :: thesis:

end;