let TS be non empty TopSpace; ( TS is T_2 & TS is compact implies TS is normal )
assume that
A1:
TS is T_2
and
A2:
TS is compact
; TS is normal
let A, B be Subset of TS; COMPTS_1:def 3 ( 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 = {}
; XBOOLE_0:def 7 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 ;
( 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
;
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
;
ex z being object st
( X in the topology of TS & z in the topology of TS & S1[x,X,z] )
take
Y
;
( 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;
S1[x,X,Y]
W /\ V = {}
by A14;
hence
S1[
x,
X,
Y]
by A10, A11, A12, A13;
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
then reconsider Cf = f .: A as Subset-Family of TS ;
A c= union Cf
then A22:
Cf is Cover of A
by SETFAM_1:def 11;
A23:
Cf is open
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
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
take W = union C; 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; ( 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; ( V is open & A c= W & B c= V & W misses V )
Bk is open
hence
V is open
by A31, TOPS_2:20; ( A c= W & B c= V & W misses V )
thus
A c= W
by A27, SETFAM_1:def 11; ( 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; W misses V
thus
W /\ V = {}
XBOOLE_0:def 7 verumproof
set x = the
Element of
(union C) /\ (meet Bk);
assume A43:
W /\ V <> {}
;
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;
verum
end;