let TS be TopSpace; :: thesis:
assume A1: TS is Hausdorff ; :: thesis:
let F be Subset of TS; :: thesis:
assume that
A2: F <> {} and
A3: F is compact ; :: thesis:
let a be Point of TS; :: thesis:
assume A4: a in F ` ; :: thesis:
A5: not a in F by A4, XBOOLE_0:def 5;
defpred S₁[ set , set , set ] means ex PS, QS being Subset of TS st
( $2 = PS & $3 = QS & PS is open & QS is open & a in PS & $1 in QS & PS /\ QS = {} );
A6: for x being set st x in F 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 A7: x in F ; :: thesis:
then reconsider p = x as Point of TS ;
consider W, V being Subset of TS such that
A8: W is open and
A9: V is open and
A10: a in W and
A11: p in V and
A12: W misses V by A1, A5, A7, PRE_TOPC:def 16;
reconsider PS = W, QS = V as set ;
take PS ; :: thesis:
take QS ; :: thesis:
thus ( PS in the topology of TS & QS in the topology of TS ) by A8, A9, PRE_TOPC:def 5; :: thesis:
take W ; :: thesis:
take V ; :: thesis:
thus ( PS = W & QS = V & W is open & V is open & a in W & x in V & W /\ V = {} ) by A8, A9, A10, A11, A12, XBOOLE_0:def 7; :: thesis:

end;

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

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in g .: F ; :: thesis:
then consider y being set such that
y in dom g and
A15: y in F and
A16: g . y = x by FUNCT_1:def 12;
ex PS, QS being Subset of TS st
( f . y = PS & g . y = QS & PS is open & QS is open & a in PS & y in QS & PS /\ QS = {} ) by A14, A15;
hence x in bool the carrier of TS by A16; :: thesis:

end;

then reconsider C = g .: F as Subset-Family of TS ;
F c= union C

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A17: x in F ; :: thesis:
then consider PS, QS being Subset of TS such that
f . x = PS and
A18: g . x = QS and
PS is open and
QS is open and
a in PS and
A19: x in QS and
PS /\ QS = {} by A14;
QS in C by A13, A17, A18, FUNCT_1:def 12;
hence x in union C by A19, TARSKI:def 4; :: thesis:

end;

then A20: C is Cover of F by SETFAM_1:def 12;
A21: C is open

let G be Subset of TS; :: according to TOPS_2:def 1 :: thesis:
assume G in C ; :: thesis:
then consider x being set such that
x in dom g and
A22: x in F and
A23: G = g . x by FUNCT_1:def 12;
ex PS, QS being Subset of TS st
( f . x = PS & g . x = QS & PS is open & QS is open & a in PS & x in QS & PS /\ QS = {} ) by A14, A22;
hence G is open by A23; :: thesis:

end;

then consider C' being Subset-Family of TS such that
A24: C' c= C and
A25: C' is Cover of F and
A26: C' is finite by A3, A20, Def7;
C' c= rng g by A13, A24, RELAT_1:146;
then consider H' being set such that
A27: H' c= dom g and
A28: H' is finite and
A29: g .: H' = C' by A26, ORDERS_1:195;
f .: H' c= bool the carrier of TS

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in f .: H' ; :: thesis:
then consider y being set such that
y in dom f and
A30: y in H' and
A31: f . y = x by FUNCT_1:def 12;
ex PS, QS being Subset of TS st
( f . y = PS & g . y = QS & PS is open & QS is open & a in PS & y in QS & PS /\ QS = {} ) by A13, A14, A27, A30;
hence x in bool the carrier of TS by A31; :: thesis:

end;

then reconsider B = f .: H' as Subset-Family of TS ;
take G0 = meet B; :: thesis:
take G1 = union C'; :: thesis:
B is open

let G be Subset of TS; :: according to TOPS_2:def 1 :: thesis:
assume G in B ; :: thesis:
then consider x being set such that
A33: x in dom f and
x in H' and
A34: G = f . x by FUNCT_1:def 12;
ex PS, QS being Subset of TS st
( f . x = PS & g . x = QS & PS is open & QS is open & a in PS & x in QS & PS /\ QS = {} ) by A13, A14, A33;
hence G is open by A34; :: thesis:

end;

hence G0 is open by A28, TOPS_2:27; :: thesis:
thus G1 is open by A21, A24, TOPS_2:18, TOPS_2:26; :: thesis:
consider z being Element of F;
F c= union C' by A25, SETFAM_1:def 12;
then z in union C' by A2, TARSKI:def 3;
then consider D being set such that
z in D and
A35: D in C' by TARSKI:def 4;
reconsider D' = D as Subset of TS by A35;
consider y being set such that
A36: y in dom g and
A37: y in H' and
D' = g . y by A29, A35, FUNCT_1:def 12;
consider PS, QS being Subset of TS such that
A38: f . y = PS and
g . y = QS and
PS is open and
QS is open and
a in PS and
y in QS and
PS /\ QS = {} by A13, A14, A36;
A39: B <> {} by A13, A36, A37, A38, FUNCT_1:def 12;
for G being set st G in B holds
a in G

let G be set ; :: thesis:
assume A40: G in B ; :: thesis:
then reconsider G' = G as Subset of TS ;
consider x being set such that
A41: x in dom f and
x in H' and
A42: G' = f . x by A40, FUNCT_1:def 12;
ex PS, QS being Subset of TS st
( f . x = PS & g . x = QS & PS is open & QS is open & a in PS & x in QS & PS /\ QS = {} ) by A13, A14, A41;
hence a in G by A42; :: thesis:

end;

hence a in G0 by A39, SETFAM_1:def 1; :: thesis:
thus F c= G1 by A25, SETFAM_1:def 12; :: thesis:
thus G0 /\ G1 = {} :: according to XBOOLE_0:def 7 :: thesis:

assume A43: G0 /\ G1 <> {} ; :: thesis:
consider x being Element of (meet B) /\ (union C');
A44: ( x in union C' & x in meet B ) by A43, XBOOLE_0:def 4;
then consider A being set such that
A45: x in A and
A46: A in C' by TARSKI:def 4;
consider z being set such that
A47: z in dom g and
A48: z in H' and
A49: A = g . z by A29, A46, FUNCT_1:def 12;
consider PS, QS being Subset of TS such that
A50: f . z = PS and
A51: g . z = QS and
PS is open and
QS is open and
a in PS and
z in QS and
A52: PS /\ QS = {} by A13, A14, A47;
PS in B by A13, A47, A48, A50, FUNCT_1:def 12;
then ( x in QS & x in PS ) by A44, A45, A49, A51, SETFAM_1:def 1;
hence contradiction by A52, XBOOLE_0:def 4; :: thesis:

end;