let T be non empty TopSpace; :: thesis:
assume A1: 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 ) ) ) ; :: thesis:
for A, B being Subset of T st A <> {} & B <> {} & A is closed & B is closed & A misses B holds
ex UA, WB being Subset of T st
( UA is open & WB is open & A c= UA & B c= WB & UA misses WB )

proof

let A, B be Subset of T; :: thesis:
assume that
A <> {} and
B <> {} and
A2: ( A is closed & B is closed ) and
A3: A misses B ; :: thesis:
set W = ([#] T) \ B;
A c= B ` by A3, SUBSET_1:23;
then consider Wn being Function of NAT,(bool the carrier of T) such that
A4: A c= Union Wn and
Union Wn c= ([#] T) \ B and
A5: for n being Element of NAT holds
( Cl (Wn . n) c= ([#] T) \ B & Wn . n is open ) by A1, A2;
set U = ([#] T) \ A;
B c= A ` by A3, SUBSET_1:23;
then consider Un being Function of NAT,(bool the carrier of T) such that
A6: B c= Union Un and
Union Un c= ([#] T) \ A and
A7: for n being Element of NAT holds
( Cl (Un . n) c= ([#] T) \ A & Un . n is open ) by A1, A2;
deffunc H₁( Element of NAT ) -> Element of bool the carrier of T = (Un . $1) \ (union { (Cl (Wn . k)) where k is Element of NAT : k in (Seg $1) \/ {0} } );
defpred S₁[ Element of NAT , set ] means $2 = H₁($1);
A8: for k being Element of NAT ex y being Subset of T st S₁[k,y] ;
consider FUW being Function of NAT,(bool the carrier of T) such that
A9: for k being Element of NAT holds S₁[k,FUW . k] from FUNCT_2:sch 3(A8);
for n being Element of NAT holds FUW . n is open

proof

let n be Element of NAT ; :: thesis:
set CLn = { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0} } ;

now

let C be set ; :: thesis:
assume C in { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0} } ; :: thesis:
then ex k being Element of NAT st
( C = Cl (Wn . k) & k in (Seg n) \/ {0} ) ;
hence C in bool the carrier of T ; :: thesis:

end;

then reconsider CLn = { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0} } as Subset-Family of T by TARSKI:def 3;
deffunc H₂( Element of NAT ) -> Element of bool the carrier of T = Cl (Wn . $1);
A10: (Seg n) \/ {0} is finite ;
A11: { H₂(k) where k is Element of NAT : k in (Seg n) \/ {0} } is finite from FRAENKEL:sch 21(A10);

now

let A be Subset of T; :: thesis:
assume A in CLn ; :: thesis:
then ex k being Element of NAT st
( A = Cl (Wn . k) & k in (Seg n) \/ {0} ) ;
hence A is closed ; :: thesis:

end;

then A12: CLn is closed by TOPS_2:def 2;
Un . n is open by A7;
then (Un . n) \ (union CLn) is open by A11, A12, Lm6, TOPS_2:21;
hence FUW . n is open by A9; :: thesis:

end;

then A13: Union FUW is open by Th17;
A14: for n being Element of NAT holds B misses Cl (Wn . n)

proof

let n be Element of NAT ; :: thesis:
Cl (Wn . n) c= ([#] T) \ B by A5;
hence B misses Cl (Wn . n) by XBOOLE_1:63, XBOOLE_1:79; :: thesis:

end;

now

let b be set ; :: thesis:
assume that
A15: b in B and
A16: not b in Union FUW ; :: thesis:
consider k being Element of NAT such that
A17: b in Un . k by A6, A15, PROB_1:12;
not b in union { (Cl (Wn . m)) where m is Element of NAT : m in (Seg k) \/ {0} }

proof

assume b in union { (Cl (Wn . m)) where m is Element of NAT : m in (Seg k) \/ {0} } ; :: thesis:
then consider CL being set such that
A18: b in CL and
A19: CL in { (Cl (Wn . m)) where m is Element of NAT : m in (Seg k) \/ {0} } by TARSKI:def 4;
consider m being Element of NAT such that
A20: CL = Cl (Wn . m) and
m in (Seg k) \/ {0} by A19;
B meets Cl (Wn . m) by A15, A18, A20, XBOOLE_0:3;
hence contradiction by A14; :: thesis:

end;

then b in H₁(k) by A17, XBOOLE_0:def 5;
then b in FUW . k by A9;
hence contradiction by A16, PROB_1:12; :: thesis:

end;

then A21: B c= Union FUW by TARSKI:def 3;
deffunc H₂( Element of NAT ) -> Element of bool the carrier of T = (Wn . $1) \ (union { (Cl (Un . k)) where k is Element of NAT : k in (Seg $1) \/ {0} } );
defpred S₂[ Element of NAT , set ] means $2 = H₂($1);
A22: for k being Element of NAT ex y being Subset of T st S₂[k,y] ;
consider FWU being Function of NAT,(bool the carrier of T) such that
A23: for k being Element of NAT holds S₂[k,FWU . k] from FUNCT_2:sch 3(A22);
A24: Union FUW misses Union FWU

proof

assume Union FUW meets Union FWU ; :: thesis:
then consider f being set such that
A25: f in Union FUW and
A26: f in Union FWU by XBOOLE_0:3;
consider n being Element of NAT such that
A27: f in FUW . n by A25, PROB_1:12;
consider k being Element of NAT such that
A28: f in FWU . k by A26, PROB_1:12;
A29: ( n >= k implies FUW . n misses FWU . k )

proof

assume that
A30: n >= k and
A31: FUW . n meets FWU . k ; :: thesis:
consider w being set such that
A32: w in FUW . n and
A33: w in FWU . k by A31, XBOOLE_0:3;
w in (Wn . k) \ (union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0} } ) by A23, A33;
then A34: w in Wn . k by XBOOLE_0:def 5;
( k = 0 or k in Seg k ) by FINSEQ_1:3;
then ( k in {0} or ( k in Seg k & Seg k c= Seg n ) ) by A30, FINSEQ_1:5, TARSKI:def 1;
then k in (Seg n) \/ {0} by XBOOLE_0:def 3;
then A35: ( Wn . k c= Cl (Wn . k) & Cl (Wn . k) in { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0} } ) by PRE_TOPC:18;
w in (Un . n) \ (union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0} } ) by A9, A32;
then not w in union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0} } by XBOOLE_0:def 5;
hence contradiction by A34, A35, TARSKI:def 4; :: thesis:

end;

( n <= k implies FUW . n misses FWU . k )

proof

assume that
A36: n <= k and
A37: FUW . n meets FWU . k ; :: thesis:
consider u being set such that
A38: u in FUW . n and
A39: u in FWU . k by A37, XBOOLE_0:3;
u in (Un . n) \ (union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0} } ) by A9, A38;
then A40: u in Un . n by XBOOLE_0:def 5;
( n = 0 or n in Seg n ) by FINSEQ_1:3;
then ( n in {0} or ( n in Seg n & Seg n c= Seg k ) ) by A36, FINSEQ_1:5, TARSKI:def 1;
then n in (Seg k) \/ {0} by XBOOLE_0:def 3;
then A41: ( Un . n c= Cl (Un . n) & Cl (Un . n) in { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0} } ) by PRE_TOPC:18;
u in (Wn . k) \ (union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0} } ) by A23, A39;
then not u in union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0} } by XBOOLE_0:def 5;
hence contradiction by A40, A41, TARSKI:def 4; :: thesis:

end;

hence contradiction by A27, A28, A29, XBOOLE_0:3; :: thesis:

end;

for n being Element of NAT holds FWU . n is open

proof

let n be Element of NAT ; :: thesis:
set CLn = { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ {0} } ;

now

let C be set ; :: thesis:
assume C in { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ {0} } ; :: thesis:
then ex k being Element of NAT st
( C = Cl (Un . k) & k in (Seg n) \/ {0} ) ;
hence C in bool the carrier of T ; :: thesis:

end;

then reconsider CLn = { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ {0} } as Subset-Family of T by TARSKI:def 3;
deffunc H₃( Element of NAT ) -> Element of bool the carrier of T = Cl (Un . $1);
A42: (Seg n) \/ {0} is finite ;
A43: { H₃(k) where k is Element of NAT : k in (Seg n) \/ {0} } is finite from FRAENKEL:sch 21(A42);

now

let A be Subset of T; :: thesis:
assume A in CLn ; :: thesis:
then ex k being Element of NAT st
( A = Cl (Un . k) & k in (Seg n) \/ {0} ) ;
hence A is closed ; :: thesis:

end;

then A44: CLn is closed by TOPS_2:def 2;
Wn . n is open by A5;
then (Wn . n) \ (union CLn) is open by A43, A44, Lm6, TOPS_2:21;
hence FWU . n is open by A23; :: thesis:

end;

then A45: Union FWU is open by Th17;
A46: for n being Element of NAT holds A misses Cl (Un . n)

proof

let n be Element of NAT ; :: thesis:
Cl (Un . n) c= ([#] T) \ A by A7;
hence A misses Cl (Un . n) by XBOOLE_1:63, XBOOLE_1:79; :: thesis:

end;

now

let a be set ; :: thesis:
assume that
A47: a in A and
A48: not a in Union FWU ; :: thesis:
consider k being Element of NAT such that
A49: a in Wn . k by A4, A47, PROB_1:12;
not a in union { (Cl (Un . m)) where m is Element of NAT : m in (Seg k) \/ {0} }

proof

assume a in union { (Cl (Un . m)) where m is Element of NAT : m in (Seg k) \/ {0} } ; :: thesis:
then consider CL being set such that
A50: a in CL and
A51: CL in { (Cl (Un . m)) where m is Element of NAT : m in (Seg k) \/ {0} } by TARSKI:def 4;
consider m being Element of NAT such that
A52: CL = Cl (Un . m) and
m in (Seg k) \/ {0} by A51;
A meets Cl (Un . m) by A47, A50, A52, XBOOLE_0:3;
hence contradiction by A46; :: thesis:

end;

then a in H₂(k) by A49, XBOOLE_0:def 5;
then a in FWU . k by A23;
hence contradiction by A48, PROB_1:12; :: thesis:

end;

then A c= Union FWU by TARSKI:def 3;
hence ex UA, WB being Subset of T st
( UA is open & WB is open & A c= UA & B c= WB & UA misses WB ) by A21, A24, A13, A45; :: thesis:

end;

hence T is normal by COMPTS_1:def 3; :: thesis: