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 )

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

hence
T is normal
; :: thesis: verum
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_{1}( 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_{1}[ Element of NAT , set ] means $2 = H_{1}($1);

A8: for k being Element of NAT ex y being Subset of T st S_{1}[k,y]
;

consider FUW being sequence of (bool the carrier of T) such that

A9: for k being Element of NAT holds S_{1}[k,FUW . k]
from FUNCT_2:sch 3(A8);

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

A14: for n being Element of NAT holds B misses Cl (Wn . n)

deffunc H_{2}( 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_{2}[ Element of NAT , set ] means $2 = H_{2}($1);

A23: for k being Element of NAT ex y being Subset of T st S_{2}[k,y]
;

consider FWU being sequence of (bool the carrier of T) such that

A24: for k being Element of NAT holds S_{2}[k,FWU . k]
from FUNCT_2:sch 3(A23);

A25: Union FUW misses Union FWU

A51: for n being Element of NAT holds A misses Cl (Un . n)

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;( 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

defpred S

A8: for k being Element of NAT ex y being Subset of T st S

consider FUW being sequence of (bool the carrier of T) such that

A9: for k being Element of NAT holds S

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

proof

then A13:
Union FUW is open
by Th17;
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} } ;

deffunc H_{2}( Element of NAT ) -> Element of bool the carrier of T = Cl (Wn . $1);

A10: (Seg n) \/ {0} is finite ;

A11: { H_{2}(k) where k is Element of NAT : k in (Seg n) \/ {0} } is finite
from FRAENKEL:sch 21(A10);

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;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

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;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;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

deffunc H

A10: (Seg n) \/ {0} is finite ;

A11: { H

now :: thesis: for A being Subset of T st A in CLn holds

A is closed

then A12:
CLn is closed
by TOPS_2:def 2;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;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

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

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;Cl (Wn . n) c= ([#] T) \ B by A5;

hence B misses Cl (Wn . n) by XBOOLE_1:63, XBOOLE_1:79; :: thesis: verum

now :: thesis: for b being object st b in B holds

b in Union FUW

then A22:
B c= Union FUW
;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} }_{1}(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;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

then
b in H
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 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

then b in FUW . k by A9, A18;

hence contradiction by A16, PROB_1:12; :: thesis: verum

deffunc H

defpred S

A23: for k being Element of NAT ex y being Subset of T st S

consider FWU being sequence of (bool the carrier of T) such that

A24: for k being Element of NAT holds S

A25: Union FUW misses Union FWU

proof

for n being Element of NAT holds FWU . n is open
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 )

end;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

( n <= k implies FUW . n misses FWU . k )
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;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

proof

hence
contradiction
by A28, A29, A30, XBOOLE_0:3; :: thesis: verum
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;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

proof

then A50:
Union FWU is open
by Th17;
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} } ;

deffunc H_{3}( Element of NAT ) -> Element of bool the carrier of T = Cl (Un . $1);

A47: (Seg n) \/ {0} is finite ;

A48: { H_{3}(k) where k is Element of NAT : k in (Seg n) \/ {0} } is finite
from FRAENKEL:sch 21(A47);

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;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

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;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;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

deffunc H

A47: (Seg n) \/ {0} is finite ;

A48: { H

now :: thesis: for A being Subset of T st A in CLn holds

A is closed

then A49:
CLn is closed
by TOPS_2:def 2;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;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

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

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;Cl (Un . n) c= ([#] T) \ A by A7;

hence A misses Cl (Un . n) by XBOOLE_1:63, XBOOLE_1:79; :: thesis: verum

now :: thesis: for a being object st a in A holds

a in Union FWU

then
A c= Union FWU
;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} }_{2}(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;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

then
a in H
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 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

then a in FWU . k by A24, A55;

hence contradiction by A53, PROB_1:12; :: thesis: verum

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