let TS be non empty TopSpace; :: thesis:
assume that
A1: TS is Hausdorff and
A2: TS is compact ; :: thesis:
let A, B be Subset of TS; :: according to COMPTS_1:def 6 :: thesis:
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:
A8: A is compact by A2, A5, Th17;
defpred S₁[ set , set , set ] 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 = {} );
A10: for x being set st x in A holds
ex y, z being set st
( y in the topology of TS & z in the topology of TS & S₁[x,y,z] )

let x be set ; :: thesis:
assume A11: x in A ; :: thesis:
then reconsider p = x as Point of TS ;
not p in B by A7, A11, XBOOLE_0:def 4;
then p in B ` by SUBSET_1:50;
then consider W, V being Subset of TS such that
A12: W is open and
A13: V is open and
A14: p in W and
A15: B c= V and
A16: W misses V by A1, A4, A2, A6, Th17, Th15;
reconsider X = W, Y = V as set ;
take X ; :: thesis:
take Y ; :: thesis:
thus ( X in the topology of TS & Y in the topology of TS ) by A12, A13, PRE_TOPC:def 5; :: thesis:
W /\ V = {} by A16, XBOOLE_0:def 7;
hence S₁[x,X,Y] by A12, A13, A14, A15; :: thesis:

end;

consider f, g being Function such that
A17: ( dom f = A & dom g = A ) and
A18: for x being set st x in A holds
S₁[x,f . x,g . x] from WELLORD2:sch 2(A10);
f .: A c= bool the carrier of TS

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in f .: A ; :: thesis:
then consider y being set such that
y in dom f and
A19: y in A and
A20: f . y = x by FUNCT_1:def 12;
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 A18, A19;
hence x in bool the carrier of TS by A20; :: thesis:

end;

then reconsider Cf = f .: A as Subset-Family of TS ;
A c= union Cf

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A21: x in A ; :: thesis:
then consider P, Q being Subset of TS such that
A22: f . x = P and
g . x = Q and
P is open and
Q is open and
A23: x in P and
( B c= Q & P /\ Q = {} ) by A18;
P in Cf by A17, A21, A22, FUNCT_1:def 12;
hence x in union Cf by A23, TARSKI:def 4; :: thesis:

end;

then A24: Cf is Cover of A by SETFAM_1:def 12;
A25: Cf is open

let G be Subset of TS; :: according to TOPS_2:def 1 :: thesis:
assume G in Cf ; :: thesis:
then consider x being set such that
x in dom f and
A26: x in A and
A27: G = f . x by FUNCT_1:def 12;
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 A18, A26;
hence G is open by A27; :: thesis:

end;

then consider C being Subset-Family of TS such that
A28: C c= Cf and
A29: C is Cover of A and
A30: C is finite by A8, A24, Def7;
C c= rng f by A17, A28, RELAT_1:146;
then consider H' being set such that
A31: H' c= dom f and
A32: H' is finite and
A33: f .: H' = C by A30, ORDERS_1:195;
g .: H' c= bool the carrier of TS

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in g .: H' ; :: thesis:
then consider y being set such that
y in dom g and
A34: y in H' and
A35: g . y = x by FUNCT_1:def 12;
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 A17, A18, A31, A34;
hence x in bool the carrier of TS by A35; :: thesis:

end;

then reconsider Bk = g .: H' as Subset-Family of TS ;
take W = union C; :: thesis:
take V = meet Bk; :: thesis:
thus W is open by A25, A28, TOPS_2:18, TOPS_2:26; :: thesis:
Bk is open

let G be Subset of TS; :: according to TOPS_2:def 1 :: thesis:
assume G in Bk ; :: thesis:
then consider x being set such that
A37: x in dom g and
x in H' and
A38: G = g . x by FUNCT_1:def 12;
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 A17, A18, A37;
hence G is open by A38; :: thesis:

end;

hence V is open by A32, TOPS_2:27; :: thesis:
thus A c= W by A29, SETFAM_1:def 12; :: thesis:
consider z being Element of A;
A c= union C by A29, SETFAM_1:def 12;
then z in union C by A3, TARSKI:def 3;
then consider D being set such that
A39: ( z in D & D in C ) by TARSKI:def 4;
consider y being set such that
A40: y in dom f and
A41: y in H' and
D = f . y by A33, A39, FUNCT_1:def 12;
consider P, Q being Subset of TS such that
f . y = P and
A42: g . y = Q and
P is open and
Q is open and
y in P and
B c= Q and
P /\ Q = {} by A17, A18, A40;
A43: Bk <> {} by A17, A40, A41, A42, FUNCT_1:def 12;
for X being set st X in Bk holds
B c= X

let X be set ; :: thesis:
assume A44: X in Bk ; :: thesis:
then reconsider X' = X as Subset of TS ;
consider x being set such that
A45: x in dom g and
x in H' and
A46: X' = g . x by A44, FUNCT_1:def 12;
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 A17, A18, A45;
hence B c= X by A46; :: thesis:

end;

hence B c= V by A43, SETFAM_1:6; :: thesis:
thus W /\ V = {} :: according to XBOOLE_0:def 7 :: thesis:

assume A47: W /\ V <> {} ; :: thesis:
consider x being Element of (union C) /\ (meet Bk);
A48: ( x in union C & x in meet Bk ) by A47, XBOOLE_0:def 4;
then consider D being set such that
A49: x in D and
A50: D in C by TARSKI:def 4;
consider z being set such that
A51: z in dom f and
A52: z in H' and
A53: D = f . z by A33, A50, FUNCT_1:def 12;
consider P, Q being Subset of TS such that
A54: f . z = P and
A55: g . z = Q and
P is open and
Q is open and
z in P and
B c= Q and
A56: P /\ Q = {} by A17, A18, A51;
Q in Bk by A17, A51, A52, A55, FUNCT_1:def 12;
then x in Q by A48, SETFAM_1:def 1;
hence contradiction by A49, A53, A54, A56, XBOOLE_0:def 4; :: thesis:

end;