let TS be TopSpace; :: thesis:
assume A1: TS is T_2 ; :: thesis:
let F be Subset of TS; :: thesis:
assume that
A2: F <> {} and
A3: F is compact ; :: thesis:
set z = the Element of F;
let a be Point of TS; :: thesis:
assume a in F ` ; :: thesis:
then A4: not a in F by XBOOLE_0:def 5;
defpred S₁[ object , object , object ] 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 = {} );
A5: for x being object st x in F holds
ex y, z being object st
( y in the topology of TS & z in the topology of TS & S₁[x,y,z] )

let x be object ; :: thesis:
assume A6: x in F ; :: thesis:
then reconsider p = x as Point of TS ;
consider W, V being Subset of TS such that
A7: W is open and
A8: V is open and
A9: a in W and
A10: p in V and
A11: W misses V by A1, A4, A6;
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 A7, A8; :: 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 A7, A8, A9, A10, A11; :: thesis:

end;

consider f, g being Function such that
A12: ( dom f = F & dom g = F ) and
A13: for x being object st x in F holds
S₁[x,f . x,g . x] from MCART_1:sch 1(A5);
g .: F c= bool the carrier of TS

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in g .: F ; :: thesis:
then consider y being object such that
y in dom g and
A14: y in F and
A15: g . y = x by FUNCT_1:def 6;
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;
hence x in bool the carrier of TS by A15; :: thesis:

end;

then reconsider C = g .: F as Subset-Family of TS ;
A16: 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 object such that
x in dom g and
A17: x in F and
A18: G = g . x by FUNCT_1:def 6;
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, A17;
hence G is open by A18; :: thesis:

end;

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in f .: H9 ; :: thesis:
then consider y being object such that
y in dom f and
A28: y in H9 and
A29: f . y = x by FUNCT_1:def 6;
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 A12, A13, A25, A28;
hence x in bool the carrier of TS by A29; :: thesis:

end;

then reconsider B = f .: H9 as Subset-Family of TS ;
take G0 = meet B; :: thesis:
take G1 = union C9; :: 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 object such that
A30: x in dom f and
x in H9 and
A31: G = f . x by FUNCT_1:def 6;
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 A12, A13, A30;
hence G is open by A31; :: thesis:

end;

let G be set ; :: thesis:
assume A33: G in B ; :: thesis:
then reconsider G9 = G as Subset of TS ;
consider x being object such that
A34: x in dom f and
x in H9 and
A35: G9 = f . x by A33, FUNCT_1:def 6;
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 A12, A13, A34;
hence a in G by A35; :: thesis:

end;

F c= union C9 by A23, SETFAM_1:def 11;
then the Element of F in union C9 by A2;
then consider D being set such that
the Element of F in D and
A36: D in C9 by TARSKI:def 4;
reconsider D9 = D as Subset of TS by A36;
consider y being object such that
A37: y in dom g and
A38: y in H9 and
D9 = g . y by A27, A36, FUNCT_1:def 6;
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 A12, A13, A37;
then B <> {} by A12, A37, A38, FUNCT_1:def 6;
hence a in G0 by A32, SETFAM_1:def 1; :: thesis:
thus F c= G1 by A23, SETFAM_1:def 11; :: thesis:
thus G0 /\ G1 = {} :: according to XBOOLE_0:def 7 :: thesis:

end;