let TS be non empty TopSpace; :: thesis: ( TS is T_2 & TS is compact implies TS is normal )

assume that

A1: TS is T_2 and

A2: TS is compact ; :: thesis: TS is normal

let A, B be Subset of TS; :: according to COMPTS_1:def 3 :: thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex P, Q being Subset of TS st

( P is open & Q is open & A c= P & B c= Q & P misses Q ) )

assume that

A3: A <> {} and

A4: B <> {} and

A5: A is closed and

A6: B is closed and

A7: A /\ B = {} ; :: according to XBOOLE_0:def 7 :: thesis: ex P, Q being Subset of TS st

( P is open & Q is open & A c= P & B c= Q & P misses Q )

defpred S_{1}[ object , object , object ] means ex P, Q being Subset of TS st

( $2 = P & $3 = Q & P is open & Q is open & $1 in P & B c= Q & P /\ Q = {} );

A8: for x being object st x in A holds

ex y, z being object st

( y in the topology of TS & z in the topology of TS & S_{1}[x,y,z] )

A15: ( dom f = A & dom g = A ) and

A16: for x being object st x in A holds

S_{1}[x,f . x,g . x]
from MCART_1:sch 1(A8);

f .: A c= bool the carrier of TS

A c= union Cf

A23: Cf is open

then consider C being Subset-Family of TS such that

A26: C c= Cf and

A27: C is Cover of A and

A28: C is finite by A22, A23;

set z = the Element of A;

A c= union C by A27, SETFAM_1:def 11;

then the Element of A in union C by A3;

then consider D being set such that

the Element of A in D and

A29: D in C by TARSKI:def 4;

C c= rng f by A15, A26, RELAT_1:113;

then consider H9 being set such that

A30: H9 c= dom f and

A31: H9 is finite and

A32: f .: H9 = C by A28, ORDERS_1:85;

g .: H9 c= bool the carrier of TS

consider y being object such that

A35: y in dom f and

A36: y in H9 and

D = f . y by A32, A29, FUNCT_1:def 6;

A37: for X being set st X in Bk holds

B c= X

( W is open & Q is open & A c= W & B c= Q & W misses Q )

take V = meet Bk; :: thesis: ( W is open & V is open & A c= W & B c= V & W misses V )

thus W is open by A23, A26, TOPS_2:11, TOPS_2:19; :: thesis: ( V is open & A c= W & B c= V & W misses V )

Bk is open

thus A c= W by A27, SETFAM_1:def 11; :: thesis: ( B c= V & W misses V )

ex P, Q being Subset of TS st

( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A15, A16, A35;

then Bk <> {} by A15, A35, A36, FUNCT_1:def 6;

hence B c= V by A37, SETFAM_1:5; :: thesis: W misses V

thus W /\ V = {} :: according to XBOOLE_0:def 7 :: thesis: verum

assume that

A1: TS is T_2 and

A2: TS is compact ; :: thesis: TS is normal

let A, B be Subset of TS; :: according to COMPTS_1:def 3 :: thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex P, Q being Subset of TS st

( P is open & Q is open & A c= P & B c= Q & P misses Q ) )

assume that

A3: A <> {} and

A4: B <> {} and

A5: A is closed and

A6: B is closed and

A7: A /\ B = {} ; :: according to XBOOLE_0:def 7 :: thesis: ex P, Q being Subset of TS st

( P is open & Q is open & A c= P & B c= Q & P misses Q )

defpred S

( $2 = P & $3 = Q & P is open & Q is open & $1 in P & B c= Q & P /\ Q = {} );

A8: for x being object st x in A holds

ex y, z being object st

( y in the topology of TS & z in the topology of TS & S

proof

consider f, g being Function such that
let x be object ; :: thesis: ( x in A implies ex y, z being object st

( y in the topology of TS & z in the topology of TS & S_{1}[x,y,z] ) )

assume A9: x in A ; :: thesis: ex y, z being object st

( y in the topology of TS & z in the topology of TS & S_{1}[x,y,z] )

then reconsider p = x as Point of TS ;

not p in B by A7, A9, XBOOLE_0:def 4;

then p in B ` by SUBSET_1:29;

then consider W, V being Subset of TS such that

A10: W is open and

A11: V is open and

A12: p in W and

A13: B c= V and

A14: W misses V by A1, A2, A4, A6, Th6, Th8;

reconsider X = W, Y = V as set ;

take X ; :: thesis: ex z being object st

( X in the topology of TS & z in the topology of TS & S_{1}[x,X,z] )

take Y ; :: thesis: ( X in the topology of TS & Y in the topology of TS & S_{1}[x,X,Y] )

thus ( X in the topology of TS & Y in the topology of TS ) by A10, A11; :: thesis: S_{1}[x,X,Y]

W /\ V = {} by A14;

hence S_{1}[x,X,Y]
by A10, A11, A12, A13; :: thesis: verum

end;( y in the topology of TS & z in the topology of TS & S

assume A9: x in A ; :: thesis: ex y, z being object st

( y in the topology of TS & z in the topology of TS & S

then reconsider p = x as Point of TS ;

not p in B by A7, A9, XBOOLE_0:def 4;

then p in B ` by SUBSET_1:29;

then consider W, V being Subset of TS such that

A10: W is open and

A11: V is open and

A12: p in W and

A13: B c= V and

A14: W misses V by A1, A2, A4, A6, Th6, Th8;

reconsider X = W, Y = V as set ;

take X ; :: thesis: ex z being object st

( X in the topology of TS & z in the topology of TS & S

take Y ; :: thesis: ( X in the topology of TS & Y in the topology of TS & S

thus ( X in the topology of TS & Y in the topology of TS ) by A10, A11; :: thesis: S

W /\ V = {} by A14;

hence S

A15: ( dom f = A & dom g = A ) and

A16: for x being object st x in A holds

S

f .: A c= bool the carrier of TS

proof

then reconsider Cf = f .: A as Subset-Family of TS ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: A or x in bool the carrier of TS )

assume x in f .: A ; :: thesis: x in bool the carrier of TS

then consider y being object such that

y in dom f and

A17: y in A and

A18: f . y = x by FUNCT_1:def 6;

ex P, Q being Subset of TS st

( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A16, A17;

hence x in bool the carrier of TS by A18; :: thesis: verum

end;assume x in f .: A ; :: thesis: x in bool the carrier of TS

then consider y being object such that

y in dom f and

A17: y in A and

A18: f . y = x by FUNCT_1:def 6;

ex P, Q being Subset of TS st

( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A16, A17;

hence x in bool the carrier of TS by A18; :: thesis: verum

A c= union Cf

proof

then A22:
Cf is Cover of A
by SETFAM_1:def 11;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in union Cf )

assume A19: x in A ; :: thesis: x in union Cf

then consider P, Q being Subset of TS such that

A20: f . x = P and

g . x = Q and

P is open and

Q is open and

A21: x in P and

B c= Q and

P /\ Q = {} by A16;

P in Cf by A15, A19, A20, FUNCT_1:def 6;

hence x in union Cf by A21, TARSKI:def 4; :: thesis: verum

end;assume A19: x in A ; :: thesis: x in union Cf

then consider P, Q being Subset of TS such that

A20: f . x = P and

g . x = Q and

P is open and

Q is open and

A21: x in P and

B c= Q and

P /\ Q = {} by A16;

P in Cf by A15, A19, A20, FUNCT_1:def 6;

hence x in union Cf by A21, TARSKI:def 4; :: thesis: verum

A23: Cf is open

proof

A is compact
by A2, A5, Th8;
let G be Subset of TS; :: according to TOPS_2:def 1 :: thesis: ( not G in Cf or G is open )

assume G in Cf ; :: thesis: G is open

then consider x being object such that

x in dom f and

A24: x in A and

A25: G = f . x by FUNCT_1:def 6;

ex P, Q being Subset of TS st

( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A16, A24;

hence G is open by A25; :: thesis: verum

end;assume G in Cf ; :: thesis: G is open

then consider x being object such that

x in dom f and

A24: x in A and

A25: G = f . x by FUNCT_1:def 6;

ex P, Q being Subset of TS st

( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A16, A24;

hence G is open by A25; :: thesis: verum

then consider C being Subset-Family of TS such that

A26: C c= Cf and

A27: C is Cover of A and

A28: C is finite by A22, A23;

set z = the Element of A;

A c= union C by A27, SETFAM_1:def 11;

then the Element of A in union C by A3;

then consider D being set such that

the Element of A in D and

A29: D in C by TARSKI:def 4;

C c= rng f by A15, A26, RELAT_1:113;

then consider H9 being set such that

A30: H9 c= dom f and

A31: H9 is finite and

A32: f .: H9 = C by A28, ORDERS_1:85;

g .: H9 c= bool the carrier of TS

proof

then reconsider Bk = g .: H9 as Subset-Family of TS ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: H9 or x in bool the carrier of TS )

assume x in g .: H9 ; :: thesis: x in bool the carrier of TS

then consider y being object such that

y in dom g and

A33: y in H9 and

A34: g . y = x by FUNCT_1:def 6;

ex P, Q being Subset of TS st

( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A15, A16, A30, A33;

hence x in bool the carrier of TS by A34; :: thesis: verum

end;assume x in g .: H9 ; :: thesis: x in bool the carrier of TS

then consider y being object such that

y in dom g and

A33: y in H9 and

A34: g . y = x by FUNCT_1:def 6;

ex P, Q being Subset of TS st

( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A15, A16, A30, A33;

hence x in bool the carrier of TS by A34; :: thesis: verum

consider y being object such that

A35: y in dom f and

A36: y in H9 and

D = f . y by A32, A29, FUNCT_1:def 6;

A37: for X being set st X in Bk holds

B c= X

proof

take W = union C; :: thesis: ex Q being Subset of TS st
let X be set ; :: thesis: ( X in Bk implies B c= X )

assume A38: X in Bk ; :: thesis: B c= X

then reconsider X9 = X as Subset of TS ;

consider x being object such that

A39: x in dom g and

x in H9 and

A40: X9 = g . x by A38, FUNCT_1:def 6;

ex P, Q being Subset of TS st

( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A15, A16, A39;

hence B c= X by A40; :: thesis: verum

end;assume A38: X in Bk ; :: thesis: B c= X

then reconsider X9 = X as Subset of TS ;

consider x being object such that

A39: x in dom g and

x in H9 and

A40: X9 = g . x by A38, FUNCT_1:def 6;

ex P, Q being Subset of TS st

( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A15, A16, A39;

hence B c= X by A40; :: thesis: verum

( W is open & Q is open & A c= W & B c= Q & W misses Q )

take V = meet Bk; :: thesis: ( W is open & V is open & A c= W & B c= V & W misses V )

thus W is open by A23, A26, TOPS_2:11, TOPS_2:19; :: thesis: ( V is open & A c= W & B c= V & W misses V )

Bk is open

proof

hence
V is open
by A31, TOPS_2:20; :: thesis: ( A c= W & B c= V & W misses V )
let G be Subset of TS; :: according to TOPS_2:def 1 :: thesis: ( not G in Bk or G is open )

assume G in Bk ; :: thesis: G is open

then consider x being object such that

A41: x in dom g and

x in H9 and

A42: G = g . x by FUNCT_1:def 6;

ex P, Q being Subset of TS st

( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A15, A16, A41;

hence G is open by A42; :: thesis: verum

end;assume G in Bk ; :: thesis: G is open

then consider x being object such that

A41: x in dom g and

x in H9 and

A42: G = g . x by FUNCT_1:def 6;

ex P, Q being Subset of TS st

( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A15, A16, A41;

hence G is open by A42; :: thesis: verum

thus A c= W by A27, SETFAM_1:def 11; :: thesis: ( B c= V & W misses V )

ex P, Q being Subset of TS st

( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A15, A16, A35;

then Bk <> {} by A15, A35, A36, FUNCT_1:def 6;

hence B c= V by A37, SETFAM_1:5; :: thesis: W misses V

thus W /\ V = {} :: according to XBOOLE_0:def 7 :: thesis: verum

proof

set x = the Element of (union C) /\ (meet Bk);

assume A43: W /\ V <> {} ; :: thesis: contradiction

then A44: the Element of (union C) /\ (meet Bk) in meet Bk by XBOOLE_0:def 4;

the Element of (union C) /\ (meet Bk) in union C by A43, XBOOLE_0:def 4;

then consider D being set such that

A45: the Element of (union C) /\ (meet Bk) in D and

A46: D in C by TARSKI:def 4;

consider z being object such that

A47: z in dom f and

A48: z in H9 and

A49: D = f . z by A32, A46, FUNCT_1:def 6;

consider P, Q being Subset of TS such that

A50: f . z = P and

A51: g . z = Q and

P is open and

Q is open and

z in P and

B c= Q and

A52: P /\ Q = {} by A15, A16, A47;

Q in Bk by A15, A47, A48, A51, FUNCT_1:def 6;

then the Element of (union C) /\ (meet Bk) in Q by A44, SETFAM_1:def 1;

hence contradiction by A45, A49, A50, A52, XBOOLE_0:def 4; :: thesis: verum

end;assume A43: W /\ V <> {} ; :: thesis: contradiction

then A44: the Element of (union C) /\ (meet Bk) in meet Bk by XBOOLE_0:def 4;

the Element of (union C) /\ (meet Bk) in union C by A43, XBOOLE_0:def 4;

then consider D being set such that

A45: the Element of (union C) /\ (meet Bk) in D and

A46: D in C by TARSKI:def 4;

consider z being object such that

A47: z in dom f and

A48: z in H9 and

A49: D = f . z by A32, A46, FUNCT_1:def 6;

consider P, Q being Subset of TS such that

A50: f . z = P and

A51: g . z = Q and

P is open and

Q is open and

z in P and

B c= Q and

A52: P /\ Q = {} by A15, A16, A47;

Q in Bk by A15, A47, A48, A51, FUNCT_1:def 6;

then the Element of (union C) /\ (meet Bk) in Q by A44, SETFAM_1:def 1;

hence contradiction by A45, A49, A50, A52, XBOOLE_0:def 4; :: thesis: verum