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 A3, SUBSET_1:23;
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 A3, SUBSET_1:23;
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 H₁( 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 sequence of (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: FUW . n is open
set CLn = { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0} } ;

now :: thesis: for C being object st C in { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0} } 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) \/ {0} } implies C in bool the carrier of T )
assume C in { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0} } ; :: thesis: C in bool the carrier of T
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: verum

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 :: 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) \/ {0} ) ;
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 A11, A12, Lm6, TOPS_2:21;
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 XBOOLE_1:63, XBOOLE_1:79; :: 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 A6, A15, PROB_1:12;
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) \/ {0} }

proof

assume b in union { (Cl (Wn . m)) where m is Element of NAT : m in (Seg k) \/ {0} } ; :: 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) \/ {0} } by TARSKI:def 4;
consider m being Element of NAT such that
A21: CL = Cl (Wn . m) and
m in (Seg k) \/ {0} by A20;
B meets Cl (Wn . m) by A15, A19, A21, XBOOLE_0:3;
hence contradiction by A14; :: thesis: verum

end;

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

end;

then A22: B c= Union FUW ;
deffunc H₂( 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);
A23: for k being Element of NAT ex y being Subset of T st S₂[k,y] ;
consider FWU being sequence of (bool the carrier of T) such that
A24: for k being Element of NAT holds S₂[k,FWU . k] from FUNCT_2:sch 3(A23);
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 A26, PROB_1:12;
consider k being Nat such that
A29: f in FWU . k by A27, PROB_1:12;
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 A32, XBOOLE_0:3;
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) \/ {0} } ) by A24, A34, A35;
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 {0} or ( k in Seg k & Seg k c= Seg n ) ) by A31, FINSEQ_1:5, TARSKI:def 1;
then k in (Seg n) \/ {0} 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) \/ {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, A33, A36;
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 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 A40, XBOOLE_0:3;
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) \/ {0} } ) 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 {0} or ( n in Seg n & Seg n c= Seg k ) ) by A39, FINSEQ_1:5, TARSKI:def 1;
then n in (Seg k) \/ {0} 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) \/ {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 A24, A42, A44;
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 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) \/ {0} } ;

now :: thesis: for C being object st C in { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ {0} } 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) \/ {0} } implies C in bool the carrier of T )
assume C in { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ {0} } ; :: thesis: C in bool the carrier of T
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: verum

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);
A47: (Seg n) \/ {0} is finite ;
A48: { H₃(k) where k is Element of NAT : k in (Seg n) \/ {0} } is finite from FRAENKEL:sch 21(A47);

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) \/ {0} ) ;
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 A48, A49, Lm6, TOPS_2:21;
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 XBOOLE_1:63, XBOOLE_1:79; :: 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 A4, A52, PROB_1:12;
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) \/ {0} }

proof

assume a in union { (Cl (Un . m)) where m is Element of NAT : m in (Seg k) \/ {0} } ; :: 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) \/ {0} } by TARSKI:def 4;
consider m being Element of NAT such that
A58: CL = Cl (Un . m) and
m in (Seg k) \/ {0} by A57;
A meets Cl (Un . m) by A52, A56, A58, XBOOLE_0:3;
hence contradiction by A51; :: thesis: verum

end;

then a in H₂(k) by A54, XBOOLE_0:def 5;
then a in FWU . k by A24, A55;
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