let TS be TopSpace; :: thesis: ( TS is T_2 implies for A being Subset of TS st A <> {} & A is compact holds
for p being Point of TS st p in A ` holds
ex PS, QS being Subset of TS st
( PS is open & QS is open & p in PS & A c= QS & PS misses QS ) )

assume A1: TS is T_2 ; :: thesis: for A being Subset of TS st A <> {} & A is compact holds
for p being Point of TS st p in A ` holds
ex PS, QS being Subset of TS st
( PS is open & QS is open & p in PS & A c= QS & PS misses QS )

let F be Subset of TS; :: thesis: ( F <> {} & F is compact implies for p being Point of TS st p in F ` holds
ex PS, QS being Subset of TS st
( PS is open & QS is open & p in PS & F c= QS & PS misses QS ) )

assume that
A2: F <> {} and
A3: F is compact ; :: thesis: for p being Point of TS st p in F ` holds
ex PS, QS being Subset of TS st
( PS is open & QS is open & p in PS & F c= QS & PS misses QS )

set z = the Element of F;
let a be Point of TS; :: thesis: ( a in F ` implies ex PS, QS being Subset of TS st
( PS is open & QS is open & a in PS & F c= QS & PS misses QS ) )

assume a in F ` ; :: thesis: ex PS, QS being Subset of TS st
( PS is open & QS is open & a in PS & F c= QS & PS misses QS )

then A4: not a in F by XBOOLE_0:def 5;
defpred S1[ 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 & S1[x,y,z] )
proof
let x be object ; :: thesis: ( x in F implies ex y, z being object st
( y in the topology of TS & z in the topology of TS & S1[x,y,z] ) )

assume A6: x in F ; :: 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 ;
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: ex z being object st
( PS in the topology of TS & z in the topology of TS & S1[x,PS,z] )

take QS ; :: thesis: ( PS in the topology of TS & QS in the topology of TS & S1[x,PS,QS] )
thus ( PS in the topology of TS & QS in the topology of TS ) by A7, A8; :: thesis: S1[x,PS,QS]
take W ; :: thesis: ex QS being Subset of TS st
( PS = W & QS = QS & W is open & QS is open & a in W & x in QS & W /\ QS = {} )

take V ; :: thesis: ( PS = W & QS = V & W is open & V is open & a in W & x in V & W /\ V = {} )
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: verum
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
S1[x,f . x,g . x] from g .: F c= bool the carrier of TS
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in g .: F or x in bool the carrier of TS )
assume x in g .: F ; :: thesis: x in bool the carrier of TS
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 ;
hence x in bool the carrier of TS by A15; :: thesis: verum
end;
then reconsider C = g .: F as Subset-Family of TS ;
A16: C is open
proof
let G be Subset of TS; :: according to TOPS_2:def 1 :: thesis: ( not G in C or G is open )
assume G in C ; :: thesis: G is open
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 ;
hence G is open by A18; :: thesis: verum
end;
F c= union C
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in union C )
assume A19: x in F ; :: thesis: x in union C
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 ;
hence x in union C by ; :: thesis: verum
end;
then C is Cover of F by SETFAM_1:def 11;
then consider C9 being Subset-Family of TS such that
A22: C9 c= C and
A23: C9 is Cover of F and
A24: C9 is finite by ;
C9 c= rng g by ;
then consider H9 being set such that
A25: H9 c= dom g and
A26: H9 is finite and
A27: g .: H9 = C9 by ;
f .: H9 c= bool the carrier of TS
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f .: H9 or x in bool the carrier of TS )
assume x in f .: H9 ; :: thesis: x in bool the carrier of TS
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: verum
end;
then reconsider B = f .: H9 as Subset-Family of TS ;
take G0 = meet B; :: thesis: ex QS being Subset of TS st
( G0 is open & QS is open & a in G0 & F c= QS & G0 misses QS )

take G1 = union C9; :: thesis: ( G0 is open & G1 is open & a in G0 & F c= G1 & G0 misses G1 )
B is open
proof
let G be Subset of TS; :: according to TOPS_2:def 1 :: thesis: ( not G in B or G is open )
assume G in B ; :: thesis: G is open
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 ;
hence G is open by A31; :: thesis: verum
end;
hence G0 is open by ; :: thesis: ( G1 is open & a in G0 & F c= G1 & G0 misses G1 )
thus G1 is open by ; :: thesis: ( a in G0 & F c= G1 & G0 misses G1 )
A32: for G being set st G in B holds
a in G
proof
let G be set ; :: thesis: ( G in B implies a in G )
assume A33: G in B ; :: thesis: a in G
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 ;
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 ;
hence a in G by A35; :: thesis: verum
end;
F c= union C9 by ;
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 ;
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 ;
then B <> {} by ;
hence a in G0 by ; :: thesis: ( F c= G1 & G0 misses G1 )
thus F c= G1 by ; :: thesis: G0 misses G1
thus G0 /\ G1 = {} :: according to XBOOLE_0:def 7 :: thesis: verum
proof
set x = the Element of (meet B) /\ (union C9);
assume A39: G0 /\ G1 <> {} ; :: thesis: contradiction
then A40: the Element of (meet B) /\ (union C9) in meet B by XBOOLE_0:def 4;
the Element of (meet B) /\ (union C9) in union C9 by ;
then consider A being set such that
A41: the Element of (meet B) /\ (union C9) in A and
A42: A in C9 by TARSKI:def 4;
consider z being object such that
A43: z in dom g and
A44: z in H9 and
A45: A = g . z by ;
consider PS, QS being Subset of TS such that
A46: f . z = PS and
A47: g . z = QS and
PS is open and
QS is open and
a in PS and
z in QS and
A48: PS /\ QS = {} by ;
PS in B by ;
then the Element of (meet B) /\ (union C9) in PS by ;
hence contradiction by A41, A45, A47, A48, XBOOLE_0:def 4; :: thesis: verum
end;