let T be non empty TopSpace; :: thesis: ( ( 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 ) ) ) ) implies T is normal )

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 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 ) ) ) ; :: thesis: T is normal
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: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex UA, WB being Subset of T st
( UA is open & WB is open & A c= UA & B c= WB & UA misses WB ) )

assume that
A <> {} and
B <> {} and
A2: ( A is closed & B is closed ) and
A3: A misses B ; :: thesis: ex UA, WB being Subset of T st
( UA is open & WB is open & A c= UA & B c= WB & UA misses WB )

set W = ([#] T) \ B;
A c= B ` by ;
then consider Wn being sequence of (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 ;
then consider Un being sequence of (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 H1( Nat) -> Element of bool the carrier of T = (Un . \$1) \ (union { (Cl (Wn . k)) where k is Element of NAT : k in (Seg \$1) \/ } );
defpred S1[ Element of NAT , set ] means \$2 = H1(\$1);
A8: for k being Element of NAT ex y being Subset of T st S1[k,y] ;
consider FUW being sequence of (bool the carrier of T) such that
A9: for k being Element of NAT holds S1[k,FUW . k] from for n being Element of NAT holds FUW . n is open
proof
let n be Element of NAT ; :: thesis: FUW . n is open
set CLn = { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ } ;
now :: thesis: for C being object st C in { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ } holds
C in bool the carrier of T
let C be object ; :: thesis: ( C in { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ } implies C in bool the carrier of T )
assume C in { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ } ; :: thesis: C in bool the carrier of T
then ex k being Element of NAT st
( C = Cl (Wn . k) & k in (Seg n) \/ ) ;
hence C in bool the carrier of T ; :: thesis: verum
end;
then reconsider CLn = { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ } as Subset-Family of T by TARSKI:def 3;
deffunc H2( Element of NAT ) -> Element of bool the carrier of T = Cl (Wn . \$1);
A10: (Seg n) \/ is finite ;
A11: { H2(k) where k is Element of NAT : k in (Seg n) \/ } is finite from
now :: thesis: for A being Subset of T st A in CLn holds
A is closed
let A be Subset of T; :: thesis: ( A in CLn implies A is closed )
assume A in CLn ; :: thesis: A is closed
then ex k being Element of NAT st
( A = Cl (Wn . k) & k in (Seg n) \/ ) ;
hence A is closed ; :: thesis: verum
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 ;
hence FUW . n is open by A9; :: thesis: verum
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: B misses Cl (Wn . n)
Cl (Wn . n) c= ([#] T) \ B by A5;
hence B misses Cl (Wn . n) by ; :: thesis: verum
end;
now :: thesis: for b being object st b in B holds
b in Union FUW
let b be object ; :: thesis: ( b in B implies b in Union FUW )
assume that
A15: b in B and
A16: not b in Union FUW ; :: thesis: contradiction
consider k being Nat such that
A17: b in Un . k by ;
A18: k in NAT by ORDINAL1:def 12;
not b in union { (Cl (Wn . m)) where m is Element of NAT : m in (Seg k) \/ }
proof
assume b in union { (Cl (Wn . m)) where m is Element of NAT : m in (Seg k) \/ } ; :: thesis: contradiction
then consider CL being set such that
A19: b in CL and
A20: CL in { (Cl (Wn . m)) where m is Element of NAT : m in (Seg k) \/ } by TARSKI:def 4;
consider m being Element of NAT such that
A21: CL = Cl (Wn . m) and
m in (Seg k) \/ by A20;
B meets Cl (Wn . m) by ;
hence contradiction by A14; :: thesis: verum
end;
then b in H1(k) by ;
then b in FUW . k by ;
hence contradiction by A16, PROB_1:12; :: thesis: verum
end;
then A22: B c= Union FUW ;
deffunc H2( Nat) -> Element of bool the carrier of T = (Wn . \$1) \ (union { (Cl (Un . k)) where k is Element of NAT : k in (Seg \$1) \/ } );
defpred S2[ Element of NAT , set ] means \$2 = H2(\$1);
A23: for k being Element of NAT ex y being Subset of T st S2[k,y] ;
consider FWU being sequence of (bool the carrier of T) such that
A24: for k being Element of NAT holds S2[k,FWU . k] from A25: Union FUW misses Union FWU
proof
assume Union FUW meets Union FWU ; :: thesis: contradiction
then consider f being object such that
A26: f in Union FUW and
A27: f in Union FWU by XBOOLE_0:3;
consider n being Nat such that
A28: f in FUW . n by ;
consider k being Nat such that
A29: f in FWU . k by ;
A30: ( n >= k implies FUW . n misses FWU . k )
proof
assume that
A31: n >= k and
A32: FUW . n meets FWU . k ; :: thesis: contradiction
consider w being object such that
A33: w in FUW . n and
A34: w in FWU . k by ;
A35: k in NAT by ORDINAL1:def 12;
A36: n in NAT by ORDINAL1:def 12;
w in (Wn . k) \ (union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ } ) by ;
then A37: w in Wn . k by XBOOLE_0:def 5;
( k = 0 or k in Seg k ) by FINSEQ_1:3;
then ( k in or ( k in Seg k & Seg k c= Seg n ) ) by ;
then k in (Seg n) \/ by XBOOLE_0:def 3;
then A38: ( Wn . k c= Cl (Wn . k) & Cl (Wn . k) in { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ } ) by PRE_TOPC:18;
w in (Un . n) \ (union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ } ) by A9, A33, A36;
then not w in union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ } by XBOOLE_0:def 5;
hence contradiction by A37, A38, TARSKI:def 4; :: thesis: verum
end;
( n <= k implies FUW . n misses FWU . k )
proof
assume that
A39: n <= k and
A40: FUW . n meets FWU . k ; :: thesis: contradiction
consider u being object such that
A41: u in FUW . n and
A42: u in FWU . k by ;
A43: n in NAT by ORDINAL1:def 12;
A44: k in NAT by ORDINAL1:def 12;
u in (Un . n) \ (union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ } ) by A9, A41, A43;
then A45: u in Un . n by XBOOLE_0:def 5;
( n = 0 or n in Seg n ) by FINSEQ_1:3;
then ( n in or ( n in Seg n & Seg n c= Seg k ) ) by ;
then n in (Seg k) \/ by XBOOLE_0:def 3;
then A46: ( Un . n c= Cl (Un . n) & Cl (Un . n) in { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ } ) by PRE_TOPC:18;
u in (Wn . k) \ (union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ } ) by ;
then not u in union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ } by XBOOLE_0:def 5;
hence contradiction by A45, A46, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A28, A29, A30, XBOOLE_0:3; :: thesis: verum
end;
for n being Element of NAT holds FWU . n is open
proof
let n be Element of NAT ; :: thesis: FWU . n is open
set CLn = { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ } ;
now :: thesis: for C being object st C in { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ } holds
C in bool the carrier of T
let C be object ; :: thesis: ( C in { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ } implies C in bool the carrier of T )
assume C in { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ } ; :: thesis: C in bool the carrier of T
then ex k being Element of NAT st
( C = Cl (Un . k) & k in (Seg n) \/ ) ;
hence C in bool the carrier of T ; :: thesis: verum
end;
then reconsider CLn = { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ } as Subset-Family of T by TARSKI:def 3;
deffunc H3( Element of NAT ) -> Element of bool the carrier of T = Cl (Un . \$1);
A47: (Seg n) \/ is finite ;
A48: { H3(k) where k is Element of NAT : k in (Seg n) \/ } is finite from
now :: thesis: for A being Subset of T st A in CLn holds
A is closed
let A be Subset of T; :: thesis: ( A in CLn implies A is closed )
assume A in CLn ; :: thesis: A is closed
then ex k being Element of NAT st
( A = Cl (Un . k) & k in (Seg n) \/ ) ;
hence A is closed ; :: thesis: verum
end;
then A49: CLn is closed by TOPS_2:def 2;
Wn . n is open by A5;
then (Wn . n) \ (union CLn) is open by ;
hence FWU . n is open by A24; :: thesis: verum
end;
then A50: Union FWU is open by Th17;
A51: for n being Element of NAT holds A misses Cl (Un . n)
proof
let n be Element of NAT ; :: thesis: A misses Cl (Un . n)
Cl (Un . n) c= ([#] T) \ A by A7;
hence A misses Cl (Un . n) by ; :: thesis: verum
end;
now :: thesis: for a being object st a in A holds
a in Union FWU
let a be object ; :: thesis: ( a in A implies a in Union FWU )
assume that
A52: a in A and
A53: not a in Union FWU ; :: thesis: contradiction
consider k being Nat such that
A54: a in Wn . k by ;
A55: k in NAT by ORDINAL1:def 12;
not a in union { (Cl (Un . m)) where m is Element of NAT : m in (Seg k) \/ }
proof
assume a in union { (Cl (Un . m)) where m is Element of NAT : m in (Seg k) \/ } ; :: thesis: contradiction
then consider CL being set such that
A56: a in CL and
A57: CL in { (Cl (Un . m)) where m is Element of NAT : m in (Seg k) \/ } by TARSKI:def 4;
consider m being Element of NAT such that
A58: CL = Cl (Un . m) and
m in (Seg k) \/ by A57;
A meets Cl (Un . m) by ;
hence contradiction by A51; :: thesis: verum
end;
then a in H2(k) by ;
then a in FWU . k by ;
hence contradiction by A53, PROB_1:12; :: thesis: verum
end;
then A c= Union FWU ;
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 A22, A25, A13, A50; :: thesis: verum
end;
hence T is normal ; :: thesis: verum