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 S1[ 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 & S1[x,y,z] )
proof
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 & S1[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 & S1[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 & S1[x,X,z] )
take Y ; :: thesis: ( X in the topology of TS & Y in the topology of TS & S1[x,X,Y] )
thus ( X in the topology of TS & Y in the topology of TS ) by A10, A11; :: thesis: S1[x,X,Y]
W /\ V = {} by A14;
hence S1[x,X,Y] by A10, A11, A12, A13; :: thesis: verum
end;
consider f, g being Function such that
A15: ( dom f = A & dom g = A ) and
A16: for x being object st x in A holds
S1[x,f . x,g . x] from MCART_1:sch 1(A8);
 f .: A c= bool the carrier of TS
proof
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;
then reconsider Cf = f .: A as Subset-Family of TS ;
A c= union Cf
proof
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;
then A22: Cf is Cover of A by SETFAM_1:def 11;
A23: Cf is open
proof
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;
A is compact by A2, A5, Th8;
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
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;
then reconsider Bk = g .: H9 as Subset-Family 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
proof
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;
take W = union C; :: thesis: ex Q being Subset of TS st
( 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
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;
hence V is open by A31, TOPS_2:20; :: thesis: ( A c= W & B c= V & W misses V )
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;