let T be non empty TopSpace; :: thesis:
let A, B be Subset of T; :: thesis:
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:
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();

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:
thus x in X by A8; :: thesis:
thus X in GX by A4, A6, A7, A8, A9; :: thesis:

end;

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

end;

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

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

proof

take X = B ` ; :: thesis:
thus x in X by A10; :: thesis:
thus X in GX by A4; :: thesis:

end;

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

end;

hence x in union GX ; :: thesis:

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:
assume A12: X in GX ; :: thesis:

now :: thesis:

per cases by A4, A12;

suppose X = B ` ; :: thesis:

hence X is open by A2; :: thesis:

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:

hence X is open ; :: thesis:

end;

hence X is open ; :: thesis:

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:
take Z = union HX; :: thesis:
union (clf HX) = Cl (union HX) by A16, A17, Th9, Th20;
hence Y is open ; :: thesis:
thus Z is open by A13, A17, TOPS_2:11, TOPS_2:19; :: thesis:
A18: for X being Subset of T st X in HX holds
A /\ (Cl X) = {}

proof

let X be Subset of T; :: thesis:
assume X in HX ; :: thesis:
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:

per cases by A4, A20;

suppose Y = B ` ; :: thesis:

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

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:

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:

end;

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

end;

A misses union (clf HX)

proof

assume A meets union (clf HX) ; :: thesis:
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:

assume x in union (clf HX) ; :: thesis:
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:

end;

hence contradiction by A26, A27; :: thesis:

end;

hence A c= Y by SUBSET_1:23; :: thesis:

now :: thesis:

let y be Point of T; :: thesis:
assume A30: y in B ; :: thesis:
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:
thus y in W by A31; :: thesis:
W meets B by A30, A31, XBOOLE_0:3;
hence W in HX by A32; :: thesis:

end;

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

end;

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