let T be non empty TopSpace; :: thesis: for A, B being Subset of T st T is paracompact & B is closed & ( for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ) holds
ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
let A, B be Subset of T; :: thesis: ( T is paracompact & B is closed & ( for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ) implies ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z ) )
assume that
A1: T is paracompact and
A2: B is closed and
A3: for x being Point of T st x in B holds
ex V, W being Subset of T st
( V is open & W is open & A c= V & x in W & V misses W ) ; :: thesis: ex Y, Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
defpred S₁[ set ] means ( $1 = B ` or ex V, W being Subset of T ex x being Point of T st
( x in B & $1 = W & V is open & W is open & A c= V & x in W & V misses W ) );
consider GX being Subset-Family of T such that
A4: for X being Subset of T holds
( X in GX iff S₁[X] ) from SUBSET_1:sch 3();

now :: thesis: for x being Point of T st x in [#] T holds
x in union GX

let x be Point of T; :: thesis: ( x in [#] T implies x in union GX )
assume x in [#] T ; :: thesis: x in union GX
then A5: x in B \/ (B `) by PRE_TOPC:2;

now :: thesis: x in union GX

per cases ( x in B or x in B ` ) by A5, XBOOLE_0:def 3;

suppose A6: x in B ; :: thesis: x in union GX

ex X being Subset of T st
( x in X & X in GX )

proof

consider V, W being Subset of T such that
A7: ( V is open & W is open & A c= V ) and
A8: x in W and
A9: V misses W by A3, A6;
take X = W; :: thesis: ( x in X & X in GX )
thus x in X by A8; :: thesis: X in GX
thus X in GX by A4, A6, A7, A8, A9; :: thesis: verum

end;

hence x in union GX by TARSKI:def 4; :: thesis: verum

end;

suppose A10: x in B ` ; :: thesis: x in union GX

ex X being Subset of T st
( x in X & X in GX )

proof

take X = B ` ; :: thesis: ( x in X & X in GX )
thus x in X by A10; :: thesis: X in GX
thus X in GX by A4; :: thesis: verum

end;

hence x in union GX by TARSKI:def 4; :: thesis: verum

end;

end;

end;

hence x in union GX ; :: thesis: verum

end;

then [#] T c= union GX ;
then [#] T = union GX by XBOOLE_0:def 10;
then A11: GX is Cover of T by SETFAM_1:45;
for X being Subset of T st X in GX holds
X is open

proof

let X be Subset of T; :: thesis: ( X in GX implies X is open )
assume A12: X in GX ; :: thesis: X is open

now :: thesis: X is open

per cases ( X = B ` or ex V, W being Subset of T ex y being Point of T st
( y in B & X = W & V is open & W is open & A c= V & y in W & V misses W ) ) by A4, A12;

suppose X = B ` ; :: thesis: X is open

hence X is open by A2; :: thesis: verum

end;

suppose ex V, W being Subset of T ex y being Point of T st
( y in B & X = W & V is open & W is open & A c= V & y in W & V misses W ) ; :: thesis: X is open

hence X is open ; :: thesis: verum

end;

end;

end;

hence X is open ; :: thesis: verum

end;

then GX is open by TOPS_2:def 1;
then consider FX being Subset-Family of T such that
A13: FX is open and
A14: FX is Cover of T and
A15: FX is_finer_than GX and
A16: FX is locally_finite by A1, A11;
set HX = { W where W is Subset of T : ( W in FX & W meets B ) } ;
A17: { W where W is Subset of T : ( W in FX & W meets B ) } c= FX by Th8;
reconsider HX = { W where W is Subset of T : ( W in FX & W meets B ) } as Subset-Family of T by Th8, TOPS_2:2;
take Y = (union (clf HX)) ` ; :: thesis: ex Z being Subset of T st
( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
take Z = union HX; :: thesis: ( Y is open & Z is open & A c= Y & B c= Z & Y misses Z )
union (clf HX) = Cl (union HX) by A16, A17, Th9, Th20;
hence Y is open ; :: thesis: ( Z is open & A c= Y & B c= Z & Y misses Z )
thus Z is open by A13, A17, TOPS_2:11, TOPS_2:19; :: thesis: ( A c= Y & B c= Z & Y misses Z )
A18: for X being Subset of T st X in HX holds
A /\ (Cl X) = {}

proof

let X be Subset of T; :: thesis: ( X in HX implies A /\ (Cl X) = {} )
assume X in HX ; :: thesis: A /\ (Cl X) = {}
then A19: ex W being Subset of T st
( W = X & W in FX & W meets B ) ;
then consider Y being set such that
A20: Y in GX and
A21: X c= Y by A15, SETFAM_1:def 2;
reconsider Y = Y as Subset of T by A20;

now :: thesis: A /\ (Cl X) = {}

per cases ( Y = B ` or ex V, W being Subset of T ex y being Point of T st
( y in B & Y = W & V is open & W is open & A c= V & y in W & V misses W ) ) by A4, A20;

suppose Y = B ` ; :: thesis: A /\ (Cl X) = {}

hence A /\ (Cl X) = {} by A19, A21, XBOOLE_1:63, XBOOLE_1:79; :: thesis: verum

end;

suppose ex V, W being Subset of T ex y being Point of T st
( y in B & Y = W & V is open & W is open & A c= V & y in W & V misses W ) ; :: thesis: A /\ (Cl X) = {}

then consider V, W being Subset of T, y being Point of T such that
y in B and
A22: Y = W and
A23: V is open and
W is open and
A24: A c= V and
y in W and
A25: V misses W ;
V misses X by A21, A22, A25, XBOOLE_1:63;
then Cl (V /\ X) = Cl ({} T) by XBOOLE_0:def 7;
then Cl (V /\ X) = {} by PRE_TOPC:22;
then Cl (V /\ (Cl X)) = {} by A23, TOPS_1:14;
then V /\ (Cl X) = {} by Th2;
then Cl X misses V by XBOOLE_0:def 7;
then A misses Cl X by A24, XBOOLE_1:63;
hence A /\ (Cl X) = {} by XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

hence A /\ (Cl X) = {} ; :: thesis: verum

end;

A misses union (clf HX)

proof

assume A meets union (clf HX) ; :: thesis: contradiction
then consider x being object such that
A26: x in A and
A27: x in union (clf HX) by XBOOLE_0:3;
reconsider x = x as Point of T by A26;

now :: thesis: ( x in union (clf HX) implies not x in A )

assume x in union (clf HX) ; :: thesis: not x in A
then consider X being set such that
A28: x in X and
A29: X in clf HX by TARSKI:def 4;
reconsider X = X as Subset of T by A29;
ex W being Subset of T st
( X = Cl W & W in HX ) by A29, Def2;
then A /\ X = {} by A18;
then A misses X by XBOOLE_0:def 7;
hence not x in A by A28, XBOOLE_0:3; :: thesis: verum

end;

hence contradiction by A26, A27; :: thesis: verum

end;

hence A c= Y by SUBSET_1:23; :: thesis: ( B c= Z & Y misses Z )

now :: thesis: for y being Point of T st y in B holds
y in Z

let y be Point of T; :: thesis: ( y in B implies y in Z )
assume A30: y in B ; :: thesis: y in Z
ex W being Subset of T st
( y in W & W in HX )

proof

consider W being Subset of T such that
A31: y in W and
A32: W in FX by A14, Th3;
take W ; :: thesis: ( y in W & W in HX )
thus y in W by A31; :: thesis: W in HX
W meets B by A30, A31, XBOOLE_0:3;
hence W in HX by A32; :: thesis: verum

end;

hence y in Z by TARSKI:def 4; :: thesis: verum

end;

hence B c= Z ; :: thesis: Y misses Z
Z c= Y ` by Th17, SETFAM_1:13;
hence Y misses Z by SUBSET_1:23; :: thesis: verum