let T be non empty TopSpace; :: thesis: for A, B being Subset of T st T is paracompact & A is closed & B is closed & A misses B & ( 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 & A is closed & B is closed & A misses B & ( 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
A is closed and
A2: B is closed and
A misses B 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();
A5: GX is Cover of T

proof

[#] T = union GX

proof

[#] T c= union GX

proof

now

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 A6: x in B \/ (B ` ) by PRE_TOPC:18;

now

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

suppose A7: 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
A8: V is open and
A9: W is open and
A10: A c= V and
A11: ( x in W & V misses W ) by A3, A7;
take X = W; :: thesis: ( x in X & X in GX )
thus x in X by A11; :: thesis: X in GX
thus X in GX by A4, A7, A8, A9, A10, A11; :: thesis: verum

end;

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

end;

suppose A12: 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 A12; :: 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;

hence [#] T c= union GX by SUBSET_1:7; :: thesis: verum

end;

hence [#] T = union GX by XBOOLE_0:def 10; :: thesis: verum

end;

hence GX is Cover of T by SETFAM_1:60; :: thesis: verum

end;

GX is open

proof

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 A13: X in GX ; :: thesis: X is open

now

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

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;

hence GX is open by TOPS_2:def 1; :: thesis: verum

end;

then consider FX being Subset-Family of T such that
A14: FX is open and
A15: FX is Cover of T and
A16: FX is_finer_than GX and
A17: FX is locally_finite by A1, A5, Def4;
set HX = { W where W is Subset of T : ( W in FX & W meets B ) } ;
A18: { W where W is Subset of T : ( W in FX & W meets B ) } c= FX by Th11;
reconsider HX = { W where W is Subset of T : ( W in FX & W meets B ) } as Subset-Family of T by Th11, TOPS_2:3;
A19: 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 consider W being Subset of T such that
A20: W = X and
A21: W in FX and
A22: W meets B ;
consider Y being set such that
A23: Y in GX and
A24: X c= Y by A16, A20, A21, SETFAM_1:def 2;
reconsider Y = Y as Subset of T by A23;

now

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, A23;

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

hence A /\ (Cl X) = {} by A20, A22, A24, 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
A25: Y = W and
A26: V is open and
W is open and
A27: A c= V and
y in W and
A28: V misses W ;
V misses X by A24, A25, A28, XBOOLE_1:63;
then Cl (V /\ X) = Cl ({} T) by XBOOLE_0:def 7;
then Cl (V /\ X) = {} by PRE_TOPC:52;
then Cl (V /\ (Cl X)) = {} by A26, TOPS_1:41;
then V /\ (Cl X) = {} by Th2;
then Cl X misses V by XBOOLE_0:def 7;
then A misses Cl X by A27, XBOOLE_1:63;
hence A /\ (Cl X) = {} by XBOOLE_0:def 7; :: thesis: verum

end;

end;

end;

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

end;

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 A17, A18, Th12, Th23;
hence Y is open ; :: thesis: ( Z is open & A c= Y & B c= Z & Y misses Z )
thus Z is open by A14, A18, TOPS_2:18, TOPS_2:26; :: thesis: ( A c= Y & B c= Z & Y misses Z )
A misses union (clf HX)

proof

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

now

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

end;

hence contradiction by A29, A30; :: thesis: verum

end;

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

proof

now

let y be Point of T; :: thesis: ( y in B implies y in Z )
assume A33: 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
A34: y in W and
A35: W in FX by A15, Th5;
A36: W meets B by A33, A34, XBOOLE_0:3;
take W ; :: thesis: ( y in W & W in HX )
thus y in W by A34; :: thesis: W in HX
thus W in HX by A35, A36; :: thesis: verum

end;

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

end;

hence B c= Z by SUBSET_1:7; :: thesis: verum

end;

thus Y misses Z :: thesis: verum

proof

Z c= Y ` by Th20, SETFAM_1:18;
hence Y misses Z by SUBSET_1:43; :: thesis: verum

end;