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 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 ) ) ) ) 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 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: 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 A2: ( A <> {} & B <> {} & A is closed & B is closed & 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 U = ([#] T) \ A;
set W = ([#] T) \ B;
( A c= B ` & B c= A ` ) by A2, SUBSET_1:43;
then A3: ( B c= ([#] T) \ A & ([#] T) \ A is open & A c= ([#] T) \ B & ([#] T) \ B is open ) by A2;
then consider Un being Function of NAT , bool the carrier of T such that
A4: ( B c= Union Un & Union Un c= ([#] T) \ A & ( for n being Element of NAT holds
( Cl (Un . n) c= ([#] T) \ A & Un . n is open ) ) ) by A1, A2;
consider Wn being Function of NAT , bool the carrier of T such that
A5: ( A c= Union Wn & Union Wn c= ([#] T) \ B & ( for n being Element of NAT holds
( Cl (Wn . n) c= ([#] T) \ B & Wn . n is open ) ) ) by A1, A2, A3;
A6: 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 A4;
hence A misses Cl (Un . n) by XBOOLE_1:63, XBOOLE_1:79; :: thesis: verum
end;
A7: 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;
deffunc H1( 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 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 FWU being Function of NAT , bool the carrier of T such that
A9: for k being Element of NAT holds S1[k,FWU . k] from FUNCT_2:sch 3(A8);
 A10: 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 } } ;
{ (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ {0 } } c= bool the carrier of T
proof
now
let C be set ; :: 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 consider k being Element of NAT such that
A11: ( C = Cl (Un . k) & k in (Seg n) \/ {0 } ) ;
thus C in bool the carrier of T by A11; :: thesis: verum
end;
hence { (Cl (Un . k)) where k is Element of NAT : k in (Seg n) \/ {0 } } c= bool the carrier of T by TARSKI:def 3; :: 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 ;
A12: (Seg n) \/ {0 } is finite ;
deffunc H2( Element of NAT ) -> Element of bool the carrier of T = Cl (Un . $1);
A13: { H2(k) where k is Element of NAT : k in (Seg n) \/ {0 } } is finite from FRAENKEL:sch 21(A12);
 CLn is closed
proof
now
let A be Subset of T; :: thesis: ( A in CLn implies A is closed )
assume A in CLn ; :: thesis: A is closed
then consider k being Element of NAT such that
A14: ( A = Cl (Un . k) & k in (Seg n) \/ {0 } ) ;
thus A is closed by A14; :: thesis: verum
end;
hence CLn is closed by TOPS_2:def 2; :: thesis: verum
end;
then ( union CLn is closed & Wn . n is open ) by A5, A13, TOPS_2:28;
then (Wn . n) \ (union CLn) is open by Lm6;
hence FWU . n is open by A9; :: thesis: verum
end;
deffunc H2( 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 S2[ Element of NAT , set ] means $2 = H2($1);
A15: for k being Element of NAT ex y being Subset of T st S2[k,y] ;
consider FUW being Function of NAT , bool the carrier of T such that
A16: for k being Element of NAT holds S2[k,FUW . k] from FUNCT_2:sch 3(A15);
 A17: 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 } } ;
{ (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0 } } c= bool the carrier of T
proof
now
let C be set ; :: 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 consider k being Element of NAT such that
A18: ( C = Cl (Wn . k) & k in (Seg n) \/ {0 } ) ;
thus C in bool the carrier of T by A18; :: thesis: verum
end;
hence { (Cl (Wn . k)) where k is Element of NAT : k in (Seg n) \/ {0 } } c= bool the carrier of T by TARSKI:def 3; :: 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 ;
A19: (Seg n) \/ {0 } is finite ;
deffunc H3( Element of NAT ) -> Element of bool the carrier of T = Cl (Wn . $1);
A20: { H3(k) where k is Element of NAT : k in (Seg n) \/ {0 } } is finite from FRAENKEL:sch 21(A19);
 CLn is closed
proof
now
let A be Subset of T; :: thesis: ( A in CLn implies A is closed )
assume A in CLn ; :: thesis: A is closed
then consider k being Element of NAT such that
A21: ( A = Cl (Wn . k) & k in (Seg n) \/ {0 } ) ;
thus A is closed by A21; :: thesis: verum
end;
hence CLn is closed by TOPS_2:def 2; :: thesis: verum
end;
then ( union CLn is closed & Un . n is open ) by A4, A20, TOPS_2:28;
then (Un . n) \ (union CLn) is open by Lm6;
hence FUW . n is open by A16; :: thesis: verum
end;
A22: A c= Union FWU
proof
now
let a be set ; :: thesis: ( a in A implies a in Union FWU )
assume A23: ( a in A & not a in Union FWU ) ; :: thesis: contradiction
then consider k being Element of NAT such that
A24: a in Wn . k by A5, PROB_1:25;
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
A25: ( a in CL & 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
A26: ( CL = Cl (Un . m) & m in (Seg k) \/ {0 } ) by A25;
A meets Cl (Un . m) by A23, A25, A26, XBOOLE_0:3;
hence contradiction by A6; :: thesis: verum
end;
then a in H1(k) by A24, XBOOLE_0:def 5;
then a in FWU . k by A9;
hence contradiction by A23, PROB_1:25; :: thesis: verum
end;
hence A c= Union FWU by TARSKI:def 3; :: thesis: verum
end;
A27: B c= Union FUW
proof
now
let b be set ; :: thesis: ( b in B implies b in Union FUW )
assume A28: ( b in B & not b in Union FUW ) ; :: thesis: contradiction
then consider k being Element of NAT such that
A29: b in Un . k by A4, PROB_1:25;
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
A30: ( b in CL & 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
A31: ( CL = Cl (Wn . m) & m in (Seg k) \/ {0 } ) by A30;
B meets Cl (Wn . m) by A28, A30, A31, XBOOLE_0:3;
hence contradiction by A7; :: thesis: verum
end;
then b in H2(k) by A29, XBOOLE_0:def 5;
then b in FUW . k by A16;
hence contradiction by A28, PROB_1:25; :: thesis: verum
end;
hence B c= Union FUW by TARSKI:def 3; :: thesis: verum
end;
A32: Union FUW misses Union FWU
proof
assume Union FUW meets Union FWU ; :: thesis: contradiction
then consider f being set such that
A33: ( f in Union FUW & f in Union FWU ) by XBOOLE_0:3;
consider n being Element of NAT such that
A34: f in FUW . n by A33, PROB_1:25;
consider k being Element of NAT such that
A35: f in FWU . k by A33, PROB_1:25;
A36: ( n <= k implies FUW . n misses FWU . k )
proof
assume A37: ( n <= k & FUW . n meets FWU . k ) ; :: thesis: contradiction
then consider u being set such that
A38: ( u in FUW . n & u in FWU . k ) by XBOOLE_0:3;
u in (Wn . k) \ (union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0 } } ) by A9, A38;
then A39: not u in union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0 } } by XBOOLE_0:def 5;
u in (Un . n) \ (union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0 } } ) by A16, A38;
then A40: ( u in Un . n & Un . n c= Cl (Un . n) ) by PRE_TOPC:48, XBOOLE_0:def 5;
( n = 0 or n in Seg n ) by FINSEQ_1:5;
then ( n in {0 } or ( n in Seg n & Seg n c= Seg k ) ) by A37, FINSEQ_1:7, TARSKI:def 1;
then n in (Seg k) \/ {0 } by XBOOLE_0:def 3;
then Cl (Un . n) in { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0 } } ;
hence contradiction by A39, A40, TARSKI:def 4; :: thesis: verum
end;
( n >= k implies FUW . n misses FWU . k )
proof
assume A41: ( n >= k & FUW . n meets FWU . k ) ; :: thesis: contradiction
then consider w being set such that
A42: ( w in FUW . n & w in FWU . k ) by XBOOLE_0:3;
w in (Un . n) \ (union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0 } } ) by A16, A42;
then A43: not w in union { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0 } } by XBOOLE_0:def 5;
w in (Wn . k) \ (union { (Cl (Un . l)) where l is Element of NAT : l in (Seg k) \/ {0 } } ) by A9, A42;
then A44: ( w in Wn . k & Wn . k c= Cl (Wn . k) ) by PRE_TOPC:48, XBOOLE_0:def 5;
( k = 0 or k in Seg k ) by FINSEQ_1:5;
then ( k in {0 } or ( k in Seg k & Seg k c= Seg n ) ) by A41, FINSEQ_1:7, TARSKI:def 1;
then k in (Seg n) \/ {0 } by XBOOLE_0:def 3;
then Cl (Wn . k) in { (Cl (Wn . l)) where l is Element of NAT : l in (Seg n) \/ {0 } } ;
hence contradiction by A43, A44, TARSKI:def 4; :: thesis: verum
end;
hence contradiction by A34, A35, A36, XBOOLE_0:3; :: thesis: verum
end;
( Union FUW is open & Union FWU is open ) by A10, A17, Th17;
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, A27, A32; :: thesis: verum
end;
hence T is normal by COMPTS_1:def 6; :: thesis: verum