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 S_{1}[ 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_{1}[x,y,z] )

A12: ( dom f = F & dom g = F ) and

A13: for x being object st x in F holds

S_{1}[x,f . x,g . x]
from MCART_1:sch 1(A5);

g .: F c= bool the carrier of TS

A16: C is open

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 A3, A16;

C9 c= rng g by A12, A22, RELAT_1:113;

then consider H9 being set such that

A25: H9 c= dom g and

A26: H9 is finite and

A27: g .: H9 = C9 by A24, ORDERS_1:85;

f .: H9 c= bool the carrier 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

thus G1 is open by A16, A22, TOPS_2:11, TOPS_2:19; :: thesis: ( a in G0 & F c= G1 & G0 misses G1 )

A32: for G being set st G in B holds

a in G

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: ( F c= G1 & G0 misses G1 )

thus F c= G1 by A23, SETFAM_1:def 11; :: thesis: G0 misses G1

thus G0 /\ G1 = {} :: according to XBOOLE_0:def 7 :: thesis: verum

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 S

( $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

proof

consider f, g being Function such that
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 & S_{1}[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 & S_{1}[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 & S_{1}[x,PS,z] )

take QS ; :: thesis: ( PS in the topology of TS & QS in the topology of TS & S_{1}[x,PS,QS] )

thus ( PS in the topology of TS & QS in the topology of TS ) by A7, A8; :: thesis: S_{1}[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;( y in the topology of TS & z in the topology of TS & S

assume A6: x in F ; :: thesis: ex y, z being object st

( y in the topology of TS & z in the topology of TS & S

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 & S

take QS ; :: thesis: ( PS in the topology of TS & QS in the topology of TS & S

thus ( PS in the topology of TS & QS in the topology of TS ) by A7, A8; :: thesis: S

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

A12: ( dom f = F & dom g = F ) and

A13: for x being object st x in F holds

S

g .: F c= bool the carrier of TS

proof

then reconsider C = g .: F as Subset-Family of TS ;
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 A13, A14;

hence x in bool the carrier of TS by A15; :: thesis: verum

end;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 A13, A14;

hence x in bool the carrier of TS by A15; :: thesis: verum

A16: C is open

proof

F c= union C
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 A13, A17;

hence G is open by A18; :: thesis: verum

end;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 A13, A17;

hence G is open by A18; :: thesis: verum

proof

then
C is Cover of F
by SETFAM_1:def 11;
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 A12, A19, A20, FUNCT_1:def 6;

hence x in union C by A21, TARSKI:def 4; :: thesis: verum

end;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 A12, A19, A20, FUNCT_1:def 6;

hence x in union C by A21, TARSKI:def 4; :: thesis: verum

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 A3, A16;

C9 c= rng g by A12, A22, RELAT_1:113;

then consider H9 being set such that

A25: H9 c= dom g and

A26: H9 is finite and

A27: g .: H9 = C9 by A24, ORDERS_1:85;

f .: H9 c= bool the carrier of TS

proof

then reconsider B = f .: H9 as Subset-Family of TS ;
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;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

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

hence
G0 is open
by A26, TOPS_2:20; :: thesis: ( G1 is open & a in G0 & F c= G1 & G0 misses G1 )
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 A12, A13, A30;

hence G is open by A31; :: thesis: verum

end;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 A12, A13, A30;

hence G is open by A31; :: thesis: verum

thus G1 is open by A16, A22, TOPS_2:11, TOPS_2:19; :: thesis: ( a in G0 & F c= G1 & G0 misses G1 )

A32: for G being set st G in B holds

a in G

proof

F c= union C9
by A23, SETFAM_1:def 11;
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 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: verum

end;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 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: verum

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: ( F c= G1 & G0 misses G1 )

thus F c= G1 by A23, SETFAM_1:def 11; :: 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 A39, XBOOLE_0:def 4;

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 A27, A42, FUNCT_1:def 6;

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 A12, A13, A43;

PS in B by A12, A43, A44, A46, FUNCT_1:def 6;

then the Element of (meet B) /\ (union C9) in PS by A40, SETFAM_1:def 1;

hence contradiction by A41, A45, A47, A48, XBOOLE_0:def 4; :: thesis: verum

end;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 A39, XBOOLE_0:def 4;

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 A27, A42, FUNCT_1:def 6;

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 A12, A13, A43;

PS in B by A12, A43, A44, A46, FUNCT_1:def 6;

then the Element of (meet B) /\ (union C9) in PS by A40, SETFAM_1:def 1;

hence contradiction by A41, A45, A47, A48, XBOOLE_0:def 4; :: thesis: verum