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

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

A11: A c= (union D1) \/ (union D2)

A17: [#] (T | A) = A by PRE_TOPC:def 5;

D1 is open

D2 is open

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

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

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

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

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

A11: A c= (union D1) \/ (union D2)

proof

A16:
Z /\ A in D1
by A7, A8;
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;

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

A17: [#] (T | A) = A by PRE_TOPC:def 5;

D1 is open

proof

then A20:
union D1 is open
by TOPS_2:19;
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;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

D2 is open

proof

then A23:
union D2 is open
by TOPS_2:19;
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;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

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