let T be TopSpace; :: thesis: for D being open mutually-disjoint Subset-Family of T
for A being Subset of T
for X being set st A is connected & X in D & X meets A & D is Cover of A holds
A c= X
let D be open mutually-disjoint Subset-Family of T; :: thesis: for A being Subset of T
for X being set st A is connected & X in D & X meets A & D is Cover of A holds
A c= X
let A be Subset of T; :: thesis: for X being set st A is connected & X in D & X meets A & D is Cover of A holds
A c= X
let X be set ; :: thesis: ( A is connected & X in D & X meets A & D is Cover of A implies A c= X )
assume that
A1: T | A is connected and
A2: X in D and
A3: X meets A ; :: according to CONNSP_1:def 3 :: thesis: ( not D is Cover of A or A c= X )
consider x being object such that
A4: ( x in X & x in A ) by A3, XBOOLE_0:3;
assume D is Cover of A ; :: thesis: A c= X
then A5: A c= union D by SETFAM_1:def 11;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in X )
assume A6: a in A ; :: thesis: a in X
then consider Z being set such that
A7: a in Z and
A8: Z in D by A5, TARSKI:def 4;
set D2 = { (K /\ A) where K is Subset of T : ( K in D & not a in K ) } ;
{ (K /\ A) where K is Subset of T : ( K in D & not a in K ) } c= bool A
proof
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in { (K /\ A) where K is Subset of T : ( K in D & not a in K ) } or d in bool A )
reconsider dd = d as set by TARSKI:1;
assume d in { (K /\ A) where K is Subset of T : ( K in D & not a in K ) } ; :: thesis: d in bool A
then ex K1 being Subset of T st
( d = K1 /\ A & K1 in D & not a in K1 ) ;
then dd c= A by XBOOLE_1:17;
hence d in bool A ; :: thesis: verum
end;
then reconsider D2 = { (K /\ A) where K is Subset of T : ( K in D & not a in K ) } as Subset-Family of (T | A) by PRE_TOPC:8;
assume not a in X ; :: thesis: contradiction
then A9: X /\ A in D2 by A2;
x in X /\ A by A4, XBOOLE_0:def 4;
then A10: x in union D2 by A9, TARSKI:def 4;
set D1 = { (K /\ A) where K is Subset of T : ( K in D & a in K ) } ;
{ (K /\ A) where K is Subset of T : ( K in D & a in K ) } c= bool A
proof
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in { (K /\ A) where K is Subset of T : ( K in D & a in K ) } or d in bool A )
reconsider dd = d as set by TARSKI:1;
assume d in { (K /\ A) where K is Subset of T : ( K in D & a in K ) } ; :: thesis: d in bool A
then ex K1 being Subset of T st
( d = K1 /\ A & K1 in D & a in K1 ) ;
then dd c= A by XBOOLE_1:17;
hence d in bool A ; :: thesis: verum
end;
then reconsider D1 = { (K /\ A) where K is Subset of T : ( K in D & a in K ) } as Subset-Family of (T | A) by PRE_TOPC:8;
A11: A c= (union D1) \/ (union D2)
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in A or b in (union D1) \/ (union D2) )
assume A12: b in A ; :: thesis: b in (union D1) \/ (union D2)
then consider Z being set such that
A13: b in Z and
A14: Z in D by A5, TARSKI:def 4;
reconsider Z = Z as Subset of T by A14;
A15: b in Z /\ A by A12, A13, XBOOLE_0:def 4;
per cases ( a in Z or not a in Z ) ;
end;
end;
A16: Z /\ A in D1 by A7, A8;
A17: [#] (T | A) = A by PRE_TOPC:def 5;
D1 is open
proof
let P be Subset of (T | A); :: according to TOPS_2:def 1 :: thesis: ( not P in D1 or P is open )
assume P in D1 ; :: thesis: P is open
then consider K1 being Subset of T such that
A18: P = K1 /\ A and
A19: K1 in D and
a in K1 ;
K1 is open by A19, TOPS_2:def 1;
hence P is open by A17, A18, TOPS_2:24; :: thesis: verum
end;
then A20: union D1 is open by TOPS_2:19;
D2 is open
proof
let P be Subset of (T | A); :: according to TOPS_2:def 1 :: thesis: ( not P in D2 or P is open )
assume P in D2 ; :: thesis: P is open
then consider K1 being Subset of T such that
A21: P = K1 /\ A and
A22: K1 in D and
not a in K1 ;
K1 is open by A22, TOPS_2:def 1;
hence P is open by A17, A21, TOPS_2:24; :: thesis: verum
end;
then A23: union D2 is open by TOPS_2:19;
the carrier of (T | A) = A by PRE_TOPC:8;
then A24: A = (union D1) \/ (union D2) by A11;
a in Z /\ A by A6, A7, XBOOLE_0:def 4;
then union D1 <> {} (T | A) by A16, TARSKI:def 4;
then union D1 meets union D2 by A1, A17, A20, A23, A24, A10, CONNSP_1:11;
then consider y being object such that
A25: y in union D1 and
A26: y in union D2 by XBOOLE_0:3;
consider Y2 being set such that
A27: y in Y2 and
A28: Y2 in D2 by A26, TARSKI:def 4;
consider K2 being Subset of T such that
A29: Y2 = K2 /\ A and
A30: ( K2 in D & not a in K2 ) by A28;
A31: y in K2 by A27, A29, XBOOLE_0:def 4;
consider Y1 being set such that
A32: y in Y1 and
A33: Y1 in D1 by A25, TARSKI:def 4;
consider K1 being Subset of T such that
A34: Y1 = K1 /\ A and
A35: ( K1 in D & a in K1 ) by A33;
y in K1 by A32, A34, XBOOLE_0:def 4;
then K1 meets K2 by A31, XBOOLE_0:3;
hence contradiction by A35, A30, TAXONOM2:def 5; :: thesis: verum