:: CONNSP_3 semantic presentation begin definition let GX be TopStruct ; let V be Subset of GX; func Component_of V -> Subset of GX means :Def1: :: CONNSP_3:def 1 ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) ) & union F = it ); existence ex b1 being Subset of GX ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) ) & union F = b1 ) proof defpred S1[ set ] means ex A1 being Subset of GX st ( A1 = \$1 & A1 is connected & V c= \$1 ); consider F being Subset-Family of GX such that A1: for A being Subset of GX holds ( A in F iff S1[A] ) from SUBSET_1:sch_3(); take union F ; ::_thesis: ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) ) & union F = union F ) take F ; ::_thesis: ( ( for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) ) & union F = union F ) thus for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) ::_thesis: union F = union F proof let A be Subset of GX; ::_thesis: ( A in F iff ( A is connected & V c= A ) ) thus ( A in F implies ( A is connected & V c= A ) ) ::_thesis: ( A is connected & V c= A implies A in F ) proof assume A in F ; ::_thesis: ( A is connected & V c= A ) then ex A1 being Subset of GX st ( A1 = A & A1 is connected & V c= A ) by A1; hence ( A is connected & V c= A ) ; ::_thesis: verum end; thus ( A is connected & V c= A implies A in F ) by A1; ::_thesis: verum end; thus union F = union F ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of GX st ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) ) & union F = b1 ) & ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) ) & union F = b2 ) holds b1 = b2 proof let S, S9 be Subset of GX; ::_thesis: ( ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) ) & union F = S ) & ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) ) & union F = S9 ) implies S = S9 ) assume that A2: ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) ) & union F = S ) and A3: ex F9 being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F9 iff ( A is connected & V c= A ) ) ) & union F9 = S9 ) ; ::_thesis: S = S9 consider F being Subset-Family of GX such that A4: for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) and A5: union F = S by A2; consider F9 being Subset-Family of GX such that A6: for A being Subset of GX holds ( A in F9 iff ( A is connected & V c= A ) ) and A7: union F9 = S9 by A3; now__::_thesis:_for_y_being_set_holds_ (_y_in_S_iff_y_in_S9_) let y be set ; ::_thesis: ( y in S iff y in S9 ) A8: now__::_thesis:_(_y_in_S9_implies_y_in_S_) assume y in S9 ; ::_thesis: y in S then consider B being set such that A9: y in B and A10: B in F9 by A7, TARSKI:def_4; reconsider B = B as Subset of GX by A10; ( B is connected & V c= B ) by A6, A10; then B in F by A4; hence y in S by A5, A9, TARSKI:def_4; ::_thesis: verum end; now__::_thesis:_(_y_in_S_implies_y_in_S9_) assume y in S ; ::_thesis: y in S9 then consider B being set such that A11: y in B and A12: B in F by A5, TARSKI:def_4; reconsider B = B as Subset of GX by A12; ( B is connected & V c= B ) by A4, A12; then B in F9 by A6; hence y in S9 by A7, A11, TARSKI:def_4; ::_thesis: verum end; hence ( y in S iff y in S9 ) by A8; ::_thesis: verum end; hence S = S9 by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def1 defines Component_of CONNSP_3:def_1_:_ for GX being TopStruct for V, b3 being Subset of GX holds ( b3 = Component_of V iff ex F being Subset-Family of GX st ( ( for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) ) & union F = b3 ) ); theorem Th1: :: CONNSP_3:1 for GX being TopSpace for V being Subset of GX st ex A being Subset of GX st ( A is connected & V c= A ) holds V c= Component_of V proof let GX be TopSpace; ::_thesis: for V being Subset of GX st ex A being Subset of GX st ( A is connected & V c= A ) holds V c= Component_of V let V be Subset of GX; ::_thesis: ( ex A being Subset of GX st ( A is connected & V c= A ) implies V c= Component_of V ) given A being Subset of GX such that A1: ( A is connected & V c= A ) ; ::_thesis: V c= Component_of V consider F being Subset-Family of GX such that A2: for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) and A3: Component_of V = union F by Def1; A4: for A being set st A in F holds V c= A by A2; F <> {} by A1, A2; then A5: V c= meet F by A4, SETFAM_1:5; meet F c= union F by SETFAM_1:2; hence V c= Component_of V by A3, A5, XBOOLE_1:1; ::_thesis: verum end; theorem :: CONNSP_3:2 for GX being TopSpace for V being Subset of GX st ( for A being Subset of GX holds ( not A is connected or not V c= A ) ) holds Component_of V = {} proof let GX be TopSpace; ::_thesis: for V being Subset of GX st ( for A being Subset of GX holds ( not A is connected or not V c= A ) ) holds Component_of V = {} let V be Subset of GX; ::_thesis: ( ( for A being Subset of GX holds ( not A is connected or not V c= A ) ) implies Component_of V = {} ) assume A1: for A being Subset of GX holds ( not A is connected or not V c= A ) ; ::_thesis: Component_of V = {} consider F being Subset-Family of GX such that A2: for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) and A3: Component_of V = union F by Def1; now__::_thesis:_not_F_<>_{} assume F <> {} ; ::_thesis: contradiction then consider A being Subset of GX such that A4: A in F by SUBSET_1:4; reconsider A = A as Subset of GX ; ( A is connected & V c= A ) by A2, A4; hence contradiction by A1; ::_thesis: verum end; hence Component_of V = {} by A3, ZFMISC_1:2; ::_thesis: verum end; theorem Th3: :: CONNSP_3:3 for GX being non empty TopSpace holds Component_of ({} GX) = the carrier of GX proof let GX be non empty TopSpace; ::_thesis: Component_of ({} GX) = the carrier of GX defpred S1[ set ] means ex A1 being Subset of GX st ( A1 = \$1 & A1 is connected & {} GX c= \$1 ); consider F being Subset-Family of GX such that A1: for A being Subset of GX holds ( A in F iff S1[A] ) from SUBSET_1:sch_3(); A2: for A being Subset of GX holds ( A in F iff ( A is connected & {} GX c= A ) ) proof let A be Subset of GX; ::_thesis: ( A in F iff ( A is connected & {} GX c= A ) ) thus ( A in F implies ( A is connected & {} GX c= A ) ) ::_thesis: ( A is connected & {} GX c= A implies A in F ) proof assume A in F ; ::_thesis: ( A is connected & {} GX c= A ) then ex A1 being Subset of GX st ( A1 = A & A1 is connected & {} GX c= A ) by A1; hence ( A is connected & {} GX c= A ) ; ::_thesis: verum end; thus ( A is connected & {} GX c= A implies A in F ) by A1; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_the_carrier_of_GX_implies_ex_Y_being_set_st_ (_x_in_Y_&_Y_in_F_)_)_&_(_ex_Y_being_set_st_ (_x_in_Y_&_Y_in_F_)_implies_x_in_the_carrier_of_GX_)_) let x be set ; ::_thesis: ( ( x in the carrier of GX implies ex Y being set st ( x in Y & Y in F ) ) & ( ex Y being set st ( x in Y & Y in F ) implies x in the carrier of GX ) ) hereby ::_thesis: ( ex Y being set st ( x in Y & Y in F ) implies x in the carrier of GX ) assume x in the carrier of GX ; ::_thesis: ex Y being set st ( x in Y & Y in F ) then reconsider p = x as Point of GX ; reconsider Y = Component_of p as set ; take Y = Y; ::_thesis: ( x in Y & Y in F ) thus x in Y by CONNSP_1:38; ::_thesis: Y in F ( Component_of p is connected & {} GX c= Y ) by XBOOLE_1:2; hence Y in F by A2; ::_thesis: verum end; given Y being set such that A3: ( x in Y & Y in F ) ; ::_thesis: x in the carrier of GX thus x in the carrier of GX by A3; ::_thesis: verum end; then union F = the carrier of GX by TARSKI:def_4; hence Component_of ({} GX) = the carrier of GX by A2, Def1; ::_thesis: verum end; theorem :: CONNSP_3:4 for GX being non empty TopSpace for V being Subset of GX st V is connected holds Component_of V <> {} proof let GX be non empty TopSpace; ::_thesis: for V being Subset of GX st V is connected holds Component_of V <> {} let V be Subset of GX; ::_thesis: ( V is connected implies Component_of V <> {} ) assume A1: V is connected ; ::_thesis: Component_of V <> {} percases ( V = {} or V <> {} ) ; suppose V = {} ; ::_thesis: Component_of V <> {} then V = {} GX ; hence Component_of V <> {} by Th3; ::_thesis: verum end; suppose V <> {} ; ::_thesis: Component_of V <> {} hence Component_of V <> {} by A1, Th1, XBOOLE_1:3; ::_thesis: verum end; end; end; theorem Th5: :: CONNSP_3:5 for GX being TopSpace for V being Subset of GX st V is connected & V <> {} holds Component_of V is connected proof let GX be TopSpace; ::_thesis: for V being Subset of GX st V is connected & V <> {} holds Component_of V is connected let V be Subset of GX; ::_thesis: ( V is connected & V <> {} implies Component_of V is connected ) assume that A1: V is connected and A2: V <> {} ; ::_thesis: Component_of V is connected consider F being Subset-Family of GX such that A3: for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) and A4: Component_of V = union F by Def1; A5: for A being set st A in F holds V c= A by A3; F <> {} by A1, A3; then V c= meet F by A5, SETFAM_1:5; then A6: meet F <> {} GX by A2; for A being Subset of GX st A in F holds A is connected by A3; hence Component_of V is connected by A4, A6, CONNSP_1:26; ::_thesis: verum end; theorem Th6: :: CONNSP_3:6 for GX being non empty TopSpace for V, C being Subset of GX st V is connected & C is connected & Component_of V c= C holds C = Component_of V proof let GX be non empty TopSpace; ::_thesis: for V, C being Subset of GX st V is connected & C is connected & Component_of V c= C holds C = Component_of V let V, C be Subset of GX; ::_thesis: ( V is connected & C is connected & Component_of V c= C implies C = Component_of V ) assume that A1: V is connected and A2: C is connected ; ::_thesis: ( not Component_of V c= C or C = Component_of V ) assume A3: Component_of V c= C ; ::_thesis: C = Component_of V consider F being Subset-Family of GX such that A4: for A being Subset of GX holds ( A in F iff ( A is connected & V c= A ) ) and A5: Component_of V = union F by Def1; V c= Component_of V by A1, Th1; then V c= C by A3, XBOOLE_1:1; then C in F by A2, A4; then C c= Component_of V by A5, ZFMISC_1:74; hence C = Component_of V by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th7: :: CONNSP_3:7 for GX being non empty TopSpace for A being Subset of GX st A is a_component holds Component_of A = A proof let GX be non empty TopSpace; ::_thesis: for A being Subset of GX st A is a_component holds Component_of A = A let A be Subset of GX; ::_thesis: ( A is a_component implies Component_of A = A ) assume A1: A is a_component ; ::_thesis: Component_of A = A then A2: A is connected ; then A3: A c= Component_of A by Th1; A <> {} GX by A1; then Component_of A is connected by A2, Th5; hence Component_of A = A by A1, A3, CONNSP_1:def_5; ::_thesis: verum end; theorem Th8: :: CONNSP_3:8 for GX being non empty TopSpace for A being Subset of GX holds ( A is a_component iff ex V being Subset of GX st ( V is connected & V <> {} & A = Component_of V ) ) proof let GX be non empty TopSpace; ::_thesis: for A being Subset of GX holds ( A is a_component iff ex V being Subset of GX st ( V is connected & V <> {} & A = Component_of V ) ) let A be Subset of GX; ::_thesis: ( A is a_component iff ex V being Subset of GX st ( V is connected & V <> {} & A = Component_of V ) ) A1: now__::_thesis:_(_A_is_a_component_implies_ex_V_being_Subset_of_GX_st_ (_V_is_connected_&_V_<>_{}_&_A_=_Component_of_V_)_) assume A2: A is a_component ; ::_thesis: ex V being Subset of GX st ( V is connected & V <> {} & A = Component_of V ) take V = A; ::_thesis: ( V is connected & V <> {} & A = Component_of V ) thus ( V is connected & V <> {} & A = Component_of V ) by A2, Th7; ::_thesis: verum end; now__::_thesis:_(_ex_V_being_Subset_of_GX_st_ (_V_is_connected_&_V_<>_{}_&_A_=_Component_of_V_)_implies_A_is_a_component_) given V being Subset of GX such that A3: ( V is connected & V <> {} & A = Component_of V ) ; ::_thesis: A is a_component ( A is connected & ( for B being Subset of GX st B is connected & A c= B holds A = B ) ) by A3, Th5, Th6; hence A is a_component by CONNSP_1:def_5; ::_thesis: verum end; hence ( A is a_component iff ex V being Subset of GX st ( V is connected & V <> {} & A = Component_of V ) ) by A1; ::_thesis: verum end; theorem :: CONNSP_3:9 for GX being non empty TopSpace for V being Subset of GX st V is connected & V <> {} holds Component_of V is a_component by Th8; theorem :: CONNSP_3:10 for GX being non empty TopSpace for A, V being Subset of GX st A is a_component & V is connected & V c= A & V <> {} holds A = Component_of V proof let GX be non empty TopSpace; ::_thesis: for A, V being Subset of GX st A is a_component & V is connected & V c= A & V <> {} holds A = Component_of V let A, V be Subset of GX; ::_thesis: ( A is a_component & V is connected & V c= A & V <> {} implies A = Component_of V ) assume that A1: A is a_component and A2: V is connected and A3: V c= A and A4: V <> {} ; ::_thesis: A = Component_of V V c= Component_of V by A2, Th1; then A5: A meets Component_of V by A3, A4, XBOOLE_1:67; assume A6: A <> Component_of V ; ::_thesis: contradiction Component_of V is a_component by A2, A4, Th8; hence contradiction by A1, A6, A5, CONNSP_1:1, CONNSP_1:34; ::_thesis: verum end; theorem Th11: :: CONNSP_3:11 for GX being non empty TopSpace for V being Subset of GX st V is connected & V <> {} holds Component_of (Component_of V) = Component_of V proof let GX be non empty TopSpace; ::_thesis: for V being Subset of GX st V is connected & V <> {} holds Component_of (Component_of V) = Component_of V let V be Subset of GX; ::_thesis: ( V is connected & V <> {} implies Component_of (Component_of V) = Component_of V ) assume ( V is connected & V <> {} ) ; ::_thesis: Component_of (Component_of V) = Component_of V then Component_of V is a_component by Th8; hence Component_of (Component_of V) = Component_of V by Th7; ::_thesis: verum end; theorem Th12: :: CONNSP_3:12 for GX being non empty TopSpace for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds Component_of A = Component_of B proof let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds Component_of A = Component_of B let A, B be Subset of GX; ::_thesis: ( A is connected & B is connected & A <> {} & A c= B implies Component_of A = Component_of B ) assume that A1: A is connected and A2: B is connected and A3: A <> {} and A4: A c= B ; ::_thesis: Component_of A = Component_of B B <> {} by A3, A4; then A5: Component_of B is connected by A2, Th5; A6: B c= Component_of B by A2, Th1; then A7: A c= Component_of B by A4, XBOOLE_1:1; A8: Component_of B c= Component_of A proof consider F being Subset-Family of GX such that A9: for D being Subset of GX holds ( D in F iff ( D is connected & A c= D ) ) and A10: union F = Component_of A by Def1; Component_of B in F by A7, A5, A9; hence Component_of B c= Component_of A by A10, ZFMISC_1:74; ::_thesis: verum end; A11: Component_of A is connected by A1, A3, Th5; Component_of A c= Component_of B proof consider F being Subset-Family of GX such that A12: for D being Subset of GX holds ( D in F iff ( D is connected & B c= D ) ) and A13: union F = Component_of B by Def1; B c= Component_of A by A6, A8, XBOOLE_1:1; then Component_of A in F by A11, A12; hence Component_of A c= Component_of B by A13, ZFMISC_1:74; ::_thesis: verum end; hence Component_of A = Component_of B by A8, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th13: :: CONNSP_3:13 for GX being non empty TopSpace for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds B c= Component_of A proof let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is connected & B is connected & A <> {} & A c= B holds B c= Component_of A let A, B be Subset of GX; ::_thesis: ( A is connected & B is connected & A <> {} & A c= B implies B c= Component_of A ) assume that A1: A is connected and A2: B is connected and A3: ( A <> {} & A c= B ) ; ::_thesis: B c= Component_of A Component_of A = Component_of B by A1, A2, A3, Th12; hence B c= Component_of A by A2, Th1; ::_thesis: verum end; theorem Th14: :: CONNSP_3:14 for GX being non empty TopSpace for A, B being Subset of GX st A is connected & A \/ B is connected & A <> {} holds A \/ B c= Component_of A proof let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is connected & A \/ B is connected & A <> {} holds A \/ B c= Component_of A let A, B be Subset of GX; ::_thesis: ( A is connected & A \/ B is connected & A <> {} implies A \/ B c= Component_of A ) assume that A1: A is connected and A2: A \/ B is connected and A3: A <> {} ; ::_thesis: A \/ B c= Component_of A Component_of (A \/ B) = Component_of A by A1, A2, A3, Th12, XBOOLE_1:7; hence A \/ B c= Component_of A by A2, Th1; ::_thesis: verum end; theorem Th15: :: CONNSP_3:15 for GX being non empty TopSpace for A being Subset of GX for p being Point of GX st A is connected & p in A holds Component_of p = Component_of A proof let GX be non empty TopSpace; ::_thesis: for A being Subset of GX for p being Point of GX st A is connected & p in A holds Component_of p = Component_of A let A be Subset of GX; ::_thesis: for p being Point of GX st A is connected & p in A holds Component_of p = Component_of A let p be Point of GX; ::_thesis: ( A is connected & p in A implies Component_of p = Component_of A ) assume that A1: A is connected and A2: p in A ; ::_thesis: Component_of p = Component_of A ( A c= Component_of A & Component_of A is a_component ) by A1, A2, Th1, Th8; hence Component_of p = Component_of A by A2, CONNSP_1:41; ::_thesis: verum end; theorem :: CONNSP_3:16 for GX being non empty TopSpace for A, B being Subset of GX st A is connected & B is connected & A meets B holds ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A ) proof let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is connected & B is connected & A meets B holds ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A ) let A, B be Subset of GX; ::_thesis: ( A is connected & B is connected & A meets B implies ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A ) ) A1: ( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7; A2: for C, D being Subset of GX st C is connected & D is connected & C /\ D <> {} holds C \/ D c= Component_of C proof let C, D be Subset of GX; ::_thesis: ( C is connected & D is connected & C /\ D <> {} implies C \/ D c= Component_of C ) assume that A3: C is connected and A4: D is connected and A5: C /\ D <> {} ; ::_thesis: C \/ D c= Component_of C C meets D by A5, XBOOLE_0:def_7; then A6: C \/ D is connected by A3, A4, CONNSP_1:1, CONNSP_1:17; C <> {} by A5; hence C \/ D c= Component_of C by A3, A6, Th14; ::_thesis: verum end; assume ( A is connected & B is connected & A /\ B <> {} ) ; :: according to XBOOLE_0:def_7 ::_thesis: ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A ) then ( A \/ B c= Component_of A & A \/ B c= Component_of B ) by A2; hence ( A \/ B c= Component_of A & A \/ B c= Component_of B & A c= Component_of B & B c= Component_of A ) by A1, XBOOLE_1:1; ::_thesis: verum end; theorem :: CONNSP_3:17 for GX being non empty TopSpace for A being Subset of GX st A is connected & A <> {} holds Cl A c= Component_of A proof let GX be non empty TopSpace; ::_thesis: for A being Subset of GX st A is connected & A <> {} holds Cl A c= Component_of A let A be Subset of GX; ::_thesis: ( A is connected & A <> {} implies Cl A c= Component_of A ) assume that A1: A is connected and A2: A <> {} ; ::_thesis: Cl A c= Component_of A Cl A is connected by A1, CONNSP_1:19; hence Cl A c= Component_of A by A1, A2, Th13, PRE_TOPC:18; ::_thesis: verum end; theorem :: CONNSP_3:18 for GX being non empty TopSpace for A, B being Subset of GX st A is a_component & B is connected & B <> {} & A misses B holds A misses Component_of B proof let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is a_component & B is connected & B <> {} & A misses B holds A misses Component_of B let A, B be Subset of GX; ::_thesis: ( A is a_component & B is connected & B <> {} & A misses B implies A misses Component_of B ) assume that A1: A is a_component and A2: ( B is connected & B <> {} ) and A3: A /\ B = {} ; :: according to XBOOLE_0:def_7 ::_thesis: A misses Component_of B A4: A is connected by A1; assume A /\ (Component_of B) <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being Point of GX such that A5: x in A /\ (Component_of B) by SUBSET_1:4; x in A by A5, XBOOLE_0:def_4; then A6: Component_of x = Component_of A by A4, Th15; A7: x in Component_of B by A5, XBOOLE_0:def_4; ( Component_of A = A & Component_of B = Component_of (Component_of B) ) by A1, A2, Th7, Th11; then (Component_of B) /\ B = {} by A2, A3, A7, A6, Th5, Th15; hence contradiction by A2, Th1, XBOOLE_1:28; ::_thesis: verum end; begin Lm1: now__::_thesis:_for_GX_being_TopStruct_ex_F_being_Subset-Family_of_GX_st_ (_(_for_B_being_Subset_of_GX_st_B_in_F_holds_ B_is_a_component_)_&_{}_GX_=_union_F_) let GX be TopStruct ; ::_thesis: ex F being Subset-Family of GX st ( ( for B being Subset of GX st B in F holds B is a_component ) & {} GX = union F ) reconsider S = {} as Subset-Family of GX by XBOOLE_1:2; for B being Subset of GX st B in S holds B is a_component ; hence ex F being Subset-Family of GX st ( ( for B being Subset of GX st B in F holds B is a_component ) & {} GX = union F ) by ZFMISC_1:2; ::_thesis: verum end; definition let GX be TopStruct ; mode a_union_of_components of GX -> Subset of GX means :Def2: :: CONNSP_3:def 2 ex F being Subset-Family of GX st ( ( for B being Subset of GX st B in F holds B is a_component ) & it = union F ); existence ex b1 being Subset of GX ex F being Subset-Family of GX st ( ( for B being Subset of GX st B in F holds B is a_component ) & b1 = union F ) proof take {} GX ; ::_thesis: ex F being Subset-Family of GX st ( ( for B being Subset of GX st B in F holds B is a_component ) & {} GX = union F ) thus ex F being Subset-Family of GX st ( ( for B being Subset of GX st B in F holds B is a_component ) & {} GX = union F ) by Lm1; ::_thesis: verum end; end; :: deftheorem Def2 defines a_union_of_components CONNSP_3:def_2_:_ for GX being TopStruct for b2 being Subset of GX holds ( b2 is a_union_of_components of GX iff ex F being Subset-Family of GX st ( ( for B being Subset of GX st B in F holds B is a_component ) & b2 = union F ) ); theorem Th19: :: CONNSP_3:19 for GX being non empty TopSpace holds {} GX is a_union_of_components of GX proof let GX be non empty TopSpace; ::_thesis: {} GX is a_union_of_components of GX thus ex F being Subset-Family of GX st ( ( for B being Subset of GX st B in F holds B is a_component ) & {} GX = union F ) by Lm1; :: according to CONNSP_3:def_2 ::_thesis: verum end; theorem Th20: :: CONNSP_3:20 for GX being non empty TopSpace for A being Subset of GX st A = the carrier of GX holds A is a_union_of_components of GX proof let GX be non empty TopSpace; ::_thesis: for A being Subset of GX st A = the carrier of GX holds A is a_union_of_components of GX let A be Subset of GX; ::_thesis: ( A = the carrier of GX implies A is a_union_of_components of GX ) { B where B is Subset of GX : B is a_component } c= bool the carrier of GX proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { B where B is Subset of GX : B is a_component } or x in bool the carrier of GX ) assume x in { B where B is Subset of GX : B is a_component } ; ::_thesis: x in bool the carrier of GX then ex B being Subset of GX st ( x = B & B is a_component ) ; hence x in bool the carrier of GX ; ::_thesis: verum end; then reconsider S = { B where B is Subset of GX : B is a_component } as Subset-Family of GX ; A1: for B being Subset of GX st B in S holds B is a_component proof let B be Subset of GX; ::_thesis: ( B in S implies B is a_component ) assume B in S ; ::_thesis: B is a_component then ex B2 being Subset of GX st ( B = B2 & B2 is a_component ) ; hence B is a_component ; ::_thesis: verum end; the carrier of GX c= union S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of GX or x in union S ) assume x in the carrier of GX ; ::_thesis: x in union S then reconsider p = x as Point of GX ; set B3 = Component_of p; Component_of p is a_component by CONNSP_1:40; then ( p in Component_of p & Component_of p in S ) by CONNSP_1:38; hence x in union S by TARSKI:def_4; ::_thesis: verum end; then A2: the carrier of GX = union S by XBOOLE_0:def_10; assume A = the carrier of GX ; ::_thesis: A is a_union_of_components of GX hence A is a_union_of_components of GX by A2, A1, Def2; ::_thesis: verum end; theorem Th21: :: CONNSP_3:21 for GX being non empty TopSpace for A being Subset of GX for p being Point of GX st p in A & A is a_union_of_components of GX holds Component_of p c= A proof let GX be non empty TopSpace; ::_thesis: for A being Subset of GX for p being Point of GX st p in A & A is a_union_of_components of GX holds Component_of p c= A let A be Subset of GX; ::_thesis: for p being Point of GX st p in A & A is a_union_of_components of GX holds Component_of p c= A let p be Point of GX; ::_thesis: ( p in A & A is a_union_of_components of GX implies Component_of p c= A ) assume that A1: p in A and A2: A is a_union_of_components of GX ; ::_thesis: Component_of p c= A consider F being Subset-Family of GX such that A3: for B being Subset of GX st B in F holds B is a_component and A4: A = union F by A2, Def2; consider X being set such that A5: p in X and A6: X in F by A1, A4, TARSKI:def_4; reconsider B2 = X as Subset of GX by A6; B2 = Component_of p by A3, A5, A6, CONNSP_1:41; hence Component_of p c= A by A4, A6, ZFMISC_1:74; ::_thesis: verum end; theorem :: CONNSP_3:22 for GX being non empty TopSpace for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX ) proof let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX ) let A, B be Subset of GX; ::_thesis: ( A is a_union_of_components of GX & B is a_union_of_components of GX implies ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX ) ) assume that A1: A is a_union_of_components of GX and A2: B is a_union_of_components of GX ; ::_thesis: ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX ) consider Fa being Subset-Family of GX such that A3: for Ba being Subset of GX st Ba in Fa holds Ba is a_component and A4: A = union Fa by A1, Def2; consider Fb being Subset-Family of GX such that A5: for Bb being Subset of GX st Bb in Fb holds Bb is a_component and A6: B = union Fb by A2, Def2; A7: for B2 being Subset of GX st B2 in Fa \/ Fb holds B2 is a_component proof let B2 be Subset of GX; ::_thesis: ( B2 in Fa \/ Fb implies B2 is a_component ) assume B2 in Fa \/ Fb ; ::_thesis: B2 is a_component then ( B2 in Fa or B2 in Fb ) by XBOOLE_0:def_3; hence B2 is a_component by A3, A5; ::_thesis: verum end; A8: A /\ B is a_union_of_components of GX proof reconsider Fd = Fa /\ Fb as Subset-Family of GX ; A9: for B4 being Subset of GX st B4 in Fd holds B4 is a_component proof let B4 be Subset of GX; ::_thesis: ( B4 in Fd implies B4 is a_component ) assume B4 in Fd ; ::_thesis: B4 is a_component then B4 in Fa by XBOOLE_0:def_4; hence B4 is a_component by A3; ::_thesis: verum end; A10: A /\ B c= union Fd proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A /\ B or x in union Fd ) assume A11: x in A /\ B ; ::_thesis: x in union Fd then x in A by XBOOLE_0:def_4; then consider F1 being set such that A12: x in F1 and A13: F1 in Fa by A4, TARSKI:def_4; reconsider C1 = F1 as Subset of GX by A13; x in B by A11, XBOOLE_0:def_4; then consider F2 being set such that A14: x in F2 and A15: F2 in Fb by A6, TARSKI:def_4; reconsider C2 = F2 as Subset of GX by A15; A16: C2 is a_component by A5, A15; C1 is a_component by A3, A13; then A17: ( C1 = C2 or C1 misses C2 ) by A16, CONNSP_1:35; F1 /\ F2 <> {} by A12, A14, XBOOLE_0:def_4; then C1 in Fa /\ Fb by A13, A15, A17, XBOOLE_0:def_4, XBOOLE_0:def_7; hence x in union Fd by A12, TARSKI:def_4; ::_thesis: verum end; union Fd c= A /\ B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Fd or x in A /\ B ) assume x in union Fd ; ::_thesis: x in A /\ B then consider X4 being set such that A18: x in X4 and A19: X4 in Fd by TARSKI:def_4; X4 in Fb by A19, XBOOLE_0:def_4; then A20: x in union Fb by A18, TARSKI:def_4; X4 in Fa by A19, XBOOLE_0:def_4; then x in union Fa by A18, TARSKI:def_4; hence x in A /\ B by A4, A6, A20, XBOOLE_0:def_4; ::_thesis: verum end; then A /\ B = union Fd by A10, XBOOLE_0:def_10; hence A /\ B is a_union_of_components of GX by A9, Def2; ::_thesis: verum end; reconsider Fc = Fa \/ Fb as Subset-Family of GX ; A \/ B = union Fc by A4, A6, ZFMISC_1:78; hence ( A \/ B is a_union_of_components of GX & A /\ B is a_union_of_components of GX ) by A7, A8, Def2; ::_thesis: verum end; theorem :: CONNSP_3:23 for GX being non empty TopSpace for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds A is a_union_of_components of GX ) holds union Fu is a_union_of_components of GX proof let GX be non empty TopSpace; ::_thesis: for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds A is a_union_of_components of GX ) holds union Fu is a_union_of_components of GX let Fu be Subset-Family of GX; ::_thesis: ( ( for A being Subset of GX st A in Fu holds A is a_union_of_components of GX ) implies union Fu is a_union_of_components of GX ) { B where B is Subset of GX : ex B2 being Subset of GX st ( B2 in Fu & B c= B2 & B is a_component ) } c= bool the carrier of GX proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { B where B is Subset of GX : ex B2 being Subset of GX st ( B2 in Fu & B c= B2 & B is a_component ) } or x in bool the carrier of GX ) assume x in { B where B is Subset of GX : ex B2 being Subset of GX st ( B2 in Fu & B c= B2 & B is a_component ) } ; ::_thesis: x in bool the carrier of GX then ex B being Subset of GX st ( x = B & ex B2 being Subset of GX st ( B2 in Fu & B c= B2 & B is a_component ) ) ; hence x in bool the carrier of GX ; ::_thesis: verum end; then reconsider F2 = { B where B is Subset of GX : ex B2 being Subset of GX st ( B2 in Fu & B c= B2 & B is a_component ) } as Subset-Family of GX ; A1: for B being Subset of GX st B in F2 holds B is a_component proof let B be Subset of GX; ::_thesis: ( B in F2 implies B is a_component ) assume B in F2 ; ::_thesis: B is a_component then ex A2 being Subset of GX st ( B = A2 & ex B2 being Subset of GX st ( B2 in Fu & A2 c= B2 & A2 is a_component ) ) ; hence B is a_component ; ::_thesis: verum end; assume A2: for A being Subset of GX st A in Fu holds A is a_union_of_components of GX ; ::_thesis: union Fu is a_union_of_components of GX A3: union Fu c= union F2 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Fu or x in union F2 ) assume x in union Fu ; ::_thesis: x in union F2 then consider X2 being set such that A4: x in X2 and A5: X2 in Fu by TARSKI:def_4; reconsider B3 = X2 as Subset of GX by A5; B3 is a_union_of_components of GX by A2, A5; then consider F being Subset-Family of GX such that A6: for B being Subset of GX st B in F holds B is a_component and A7: B3 = union F by Def2; consider Y2 being set such that A8: x in Y2 and A9: Y2 in F by A4, A7, TARSKI:def_4; reconsider A3 = Y2 as Subset of GX by A9; ( A3 is a_component & Y2 c= B3 ) by A6, A7, A9, ZFMISC_1:74; then A3 in F2 by A5; hence x in union F2 by A8, TARSKI:def_4; ::_thesis: verum end; union F2 c= union Fu proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F2 or x in union Fu ) assume x in union F2 ; ::_thesis: x in union Fu then consider X being set such that A10: x in X and A11: X in F2 by TARSKI:def_4; ex B being Subset of GX st ( X = B & ex B2 being Subset of GX st ( B2 in Fu & B c= B2 & B is a_component ) ) by A11; hence x in union Fu by A10, TARSKI:def_4; ::_thesis: verum end; then union Fu = union F2 by A3, XBOOLE_0:def_10; hence union Fu is a_union_of_components of GX by A1, Def2; ::_thesis: verum end; theorem :: CONNSP_3:24 for GX being non empty TopSpace for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds A is a_union_of_components of GX ) holds meet Fu is a_union_of_components of GX proof let GX be non empty TopSpace; ::_thesis: for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds A is a_union_of_components of GX ) holds meet Fu is a_union_of_components of GX let Fu be Subset-Family of GX; ::_thesis: ( ( for A being Subset of GX st A in Fu holds A is a_union_of_components of GX ) implies meet Fu is a_union_of_components of GX ) assume A1: for A being Subset of GX st A in Fu holds A is a_union_of_components of GX ; ::_thesis: meet Fu is a_union_of_components of GX now__::_thesis:_(_(_Fu_<>_{}_&_meet_Fu_is_a_union_of_components_of_GX_)_or_(_Fu_=_{}_&_meet_Fu_is_a_union_of_components_of_GX_)_) percases ( Fu <> {} or Fu = {} ) ; caseA2: Fu <> {} ; ::_thesis: meet Fu is a_union_of_components of GX { B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds B c= A2 ) ) } c= bool the carrier of GX proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds B c= A2 ) ) } or x in bool the carrier of GX ) assume x in { B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds B c= A2 ) ) } ; ::_thesis: x in bool the carrier of GX then ex B being Subset of GX st ( x = B & B is a_component & ( for A2 being Subset of GX st A2 in Fu holds B c= A2 ) ) ; hence x in bool the carrier of GX ; ::_thesis: verum end; then reconsider F1 = { B where B is Subset of GX : ( B is a_component & ( for A2 being Subset of GX st A2 in Fu holds B c= A2 ) ) } as Subset-Family of GX ; A3: meet Fu c= union F1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet Fu or x in union F1 ) consider Y2 being set such that A4: Y2 in Fu by A2, XBOOLE_0:def_1; reconsider B2 = Y2 as Subset of GX by A4; B2 is a_union_of_components of GX by A1, A4; then consider F being Subset-Family of GX such that A5: for B being Subset of GX st B in F holds B is a_component and A6: B2 = union F by Def2; assume A7: x in meet Fu ; ::_thesis: x in union F1 then x in Y2 by A4, SETFAM_1:def_1; then consider Y3 being set such that A8: x in Y3 and A9: Y3 in F by A6, TARSKI:def_4; reconsider B3 = Y3 as Subset of GX by A9; A10: for A2 being Subset of GX st A2 in Fu holds B3 c= A2 proof reconsider p = x as Point of GX by A7; let A2 be Subset of GX; ::_thesis: ( A2 in Fu implies B3 c= A2 ) assume A11: A2 in Fu ; ::_thesis: B3 c= A2 then x in A2 by A7, SETFAM_1:def_1; then Component_of p c= A2 by A1, A11, Th21; hence B3 c= A2 by A5, A8, A9, CONNSP_1:41; ::_thesis: verum end; B3 is a_component by A5, A9; then Y3 in F1 by A10; hence x in union F1 by A8, TARSKI:def_4; ::_thesis: verum end; A12: for B being Subset of GX st B in F1 holds B is a_component proof let B be Subset of GX; ::_thesis: ( B in F1 implies B is a_component ) assume B in F1 ; ::_thesis: B is a_component then ex B1 being Subset of GX st ( B = B1 & B1 is a_component & ( for A2 being Subset of GX st A2 in Fu holds B1 c= A2 ) ) ; hence B is a_component ; ::_thesis: verum end; union F1 c= meet Fu proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F1 or x in meet Fu ) assume x in union F1 ; ::_thesis: x in meet Fu then consider X being set such that A13: x in X and A14: X in F1 by TARSKI:def_4; consider B being Subset of GX such that A15: X = B and B is a_component and A16: for A2 being Subset of GX st A2 in Fu holds B c= A2 by A14; for Y being set st Y in Fu holds x in Y proof let Y be set ; ::_thesis: ( Y in Fu implies x in Y ) assume Y in Fu ; ::_thesis: x in Y then B c= Y by A16; hence x in Y by A13, A15; ::_thesis: verum end; hence x in meet Fu by A2, SETFAM_1:def_1; ::_thesis: verum end; then meet Fu = union F1 by A3, XBOOLE_0:def_10; hence meet Fu is a_union_of_components of GX by A12, Def2; ::_thesis: verum end; case Fu = {} ; ::_thesis: meet Fu is a_union_of_components of GX then meet Fu = {} GX by SETFAM_1:def_1; hence meet Fu is a_union_of_components of GX by Th19; ::_thesis: verum end; end; end; hence meet Fu is a_union_of_components of GX ; ::_thesis: verum end; theorem :: CONNSP_3:25 for GX being non empty TopSpace for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds A \ B is a_union_of_components of GX proof let GX be non empty TopSpace; ::_thesis: for A, B being Subset of GX st A is a_union_of_components of GX & B is a_union_of_components of GX holds A \ B is a_union_of_components of GX let A, B be Subset of GX; ::_thesis: ( A is a_union_of_components of GX & B is a_union_of_components of GX implies A \ B is a_union_of_components of GX ) assume that A1: A is a_union_of_components of GX and A2: B is a_union_of_components of GX ; ::_thesis: A \ B is a_union_of_components of GX consider Fa being Subset-Family of GX such that A3: for B2 being Subset of GX st B2 in Fa holds B2 is a_component and A4: A = union Fa by A1, Def2; consider Fb being Subset-Family of GX such that A5: for B3 being Subset of GX st B3 in Fb holds B3 is a_component and A6: B = union Fb by A2, Def2; reconsider Fd = Fa \ Fb as Subset-Family of GX ; A7: union Fd c= A \ B proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union Fd or x in A \ B ) assume x in union Fd ; ::_thesis: x in A \ B then consider X being set such that A8: x in X and A9: X in Fd by TARSKI:def_4; reconsider A2 = X as Subset of GX by A9; A10: not X in Fb by A9, XBOOLE_0:def_5; A11: X in Fa by A9, XBOOLE_0:def_5; then A12: A2 is a_component by A3; A13: now__::_thesis:_not_x_in_B assume x in B ; ::_thesis: contradiction then consider Y3 being set such that A14: x in Y3 and A15: Y3 in Fb by A6, TARSKI:def_4; reconsider B3 = Y3 as Subset of GX by A15; A2 /\ B3 <> {} by A8, A14, XBOOLE_0:def_4; then A16: A2 meets B3 by XBOOLE_0:def_7; B3 is a_component by A5, A15; hence contradiction by A10, A12, A15, A16, CONNSP_1:35; ::_thesis: verum end; A2 c= A by A4, A11, ZFMISC_1:74; hence x in A \ B by A8, A13, XBOOLE_0:def_5; ::_thesis: verum end; A17: for B4 being Subset of GX st B4 in Fd holds B4 is a_component proof let B4 be Subset of GX; ::_thesis: ( B4 in Fd implies B4 is a_component ) assume B4 in Fd ; ::_thesis: B4 is a_component then B4 in Fa by XBOOLE_0:def_5; hence B4 is a_component by A3; ::_thesis: verum end; A \ B c= union Fd proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A \ B or x in union Fd ) assume A18: x in A \ B ; ::_thesis: x in union Fd then x in A by XBOOLE_0:def_5; then consider X being set such that A19: x in X and A20: X in Fa by A4, TARSKI:def_4; reconsider A2 = X as Subset of GX by A20; now__::_thesis:_not_A2_in_Fb assume A2 in Fb ; ::_thesis: contradiction then A2 c= B by A6, ZFMISC_1:74; hence contradiction by A18, A19, XBOOLE_0:def_5; ::_thesis: verum end; then A2 in Fd by A20, XBOOLE_0:def_5; hence x in union Fd by A19, TARSKI:def_4; ::_thesis: verum end; then A \ B = union Fd by A7, XBOOLE_0:def_10; hence A \ B is a_union_of_components of GX by A17, Def2; ::_thesis: verum end; begin definition let GX be TopStruct ; let B be Subset of GX; let p be Point of GX; assume A1: p in B ; func Down (p,B) -> Point of (GX | B) equals :Def3: :: CONNSP_3:def 3 p; coherence p is Point of (GX | B) proof B = [#] (GX | B) by PRE_TOPC:def_5; hence p is Point of (GX | B) by A1; ::_thesis: verum end; end; :: deftheorem Def3 defines Down CONNSP_3:def_3_:_ for GX being TopStruct for B being Subset of GX for p being Point of GX st p in B holds Down (p,B) = p; definition let GX be TopStruct ; let B be Subset of GX; let p be Point of (GX | B); assume A1: B <> {} ; func Up p -> Point of GX equals :: CONNSP_3:def 4 p; coherence p is Point of GX proof B = the carrier of (GX | B) by PRE_TOPC:8; then p in B by A1; hence p is Point of GX ; ::_thesis: verum end; end; :: deftheorem defines Up CONNSP_3:def_4_:_ for GX being TopStruct for B being Subset of GX for p being Point of (GX | B) st B <> {} holds Up p = p; definition let GX be TopStruct ; let V, B be Subset of GX; func Down (V,B) -> Subset of (GX | B) equals :: CONNSP_3:def 5 V /\ B; coherence V /\ B is Subset of (GX | B) proof B = [#] (GX | B) by PRE_TOPC:def_5; hence V /\ B is Subset of (GX | B) by XBOOLE_1:17; ::_thesis: verum end; end; :: deftheorem defines Down CONNSP_3:def_5_:_ for GX being TopStruct for V, B being Subset of GX holds Down (V,B) = V /\ B; definition let GX be TopStruct ; let B be Subset of GX; let V be Subset of (GX | B); func Up V -> Subset of GX equals :: CONNSP_3:def 6 V; coherence V is Subset of GX proof B = the carrier of (GX | B) by PRE_TOPC:8; hence V is Subset of GX by XBOOLE_1:1; ::_thesis: verum end; end; :: deftheorem defines Up CONNSP_3:def_6_:_ for GX being TopStruct for B being Subset of GX for V being Subset of (GX | B) holds Up V = V; definition let GX be TopStruct ; let B be Subset of GX; let p be Point of GX; assume A1: p in B ; func Component_of (p,B) -> Subset of GX means :Def7: :: CONNSP_3:def 7 for q being Point of (GX | B) st q = p holds it = Component_of q; existence ex b1 being Subset of GX st for q being Point of (GX | B) st q = p holds b1 = Component_of q proof A2: B = [#] (GX | B) by PRE_TOPC:def_5; then reconsider q3 = p as Point of (GX | B) by A1; reconsider C = Component_of q3 as Subset of GX by A2, XBOOLE_1:1; take C ; ::_thesis: for q being Point of (GX | B) st q = p holds C = Component_of q thus for q being Point of (GX | B) st q = p holds C = Component_of q ; ::_thesis: verum end; uniqueness for b1, b2 being Subset of GX st ( for q being Point of (GX | B) st q = p holds b1 = Component_of q ) & ( for q being Point of (GX | B) st q = p holds b2 = Component_of q ) holds b1 = b2 proof B = [#] (GX | B) by PRE_TOPC:def_5; then reconsider q3 = p as Point of (GX | B) by A1; let S, S9 be Subset of GX; ::_thesis: ( ( for q being Point of (GX | B) st q = p holds S = Component_of q ) & ( for q being Point of (GX | B) st q = p holds S9 = Component_of q ) implies S = S9 ) assume that A3: for q being Point of (GX | B) st q = p holds S = Component_of q and A4: for q2 being Point of (GX | B) st q2 = p holds S9 = Component_of q2 ; ::_thesis: S = S9 S = Component_of q3 by A3; hence S = S9 by A4; ::_thesis: verum end; end; :: deftheorem Def7 defines Component_of CONNSP_3:def_7_:_ for GX being TopStruct for B being Subset of GX for p being Point of GX st p in B holds for b4 being Subset of GX holds ( b4 = Component_of (p,B) iff for q being Point of (GX | B) st q = p holds b4 = Component_of q ); theorem :: CONNSP_3:26 for GX being non empty TopSpace for B being Subset of GX for p being Point of GX st p in B holds p in Component_of (p,B) proof let GX be non empty TopSpace; ::_thesis: for B being Subset of GX for p being Point of GX st p in B holds p in Component_of (p,B) let B be Subset of GX; ::_thesis: for p being Point of GX st p in B holds p in Component_of (p,B) let p be Point of GX; ::_thesis: ( p in B implies p in Component_of (p,B) ) assume A1: p in B ; ::_thesis: p in Component_of (p,B) then reconsider B9 = B as non empty Subset of GX ; reconsider q = p as Point of (GX | B9) by A1, PRE_TOPC:8; q in Component_of q by CONNSP_1:38; hence p in Component_of (p,B) by A1, Def7; ::_thesis: verum end; theorem Th27: :: CONNSP_3:27 for GX being non empty TopSpace for B being Subset of GX for p being Point of GX st p in B holds Component_of (p,B) = Component_of (Down (p,B)) proof let GX be non empty TopSpace; ::_thesis: for B being Subset of GX for p being Point of GX st p in B holds Component_of (p,B) = Component_of (Down (p,B)) let B be Subset of GX; ::_thesis: for p being Point of GX st p in B holds Component_of (p,B) = Component_of (Down (p,B)) let p be Point of GX; ::_thesis: ( p in B implies Component_of (p,B) = Component_of (Down (p,B)) ) assume A1: p in B ; ::_thesis: Component_of (p,B) = Component_of (Down (p,B)) then p = Down (p,B) by Def3; hence Component_of (p,B) = Component_of (Down (p,B)) by A1, Def7; ::_thesis: verum end; theorem :: CONNSP_3:28 for GX being TopSpace for V, B being Subset of GX st V is open holds Down (V,B) is open proof let GX be TopSpace; ::_thesis: for V, B being Subset of GX st V is open holds Down (V,B) is open let V, B be Subset of GX; ::_thesis: ( V is open implies Down (V,B) is open ) assume V is open ; ::_thesis: Down (V,B) is open then A1: V in the topology of GX by PRE_TOPC:def_2; Down (V,B) = V /\ ([#] (GX | B)) by PRE_TOPC:def_5; then Down (V,B) in the topology of (GX | B) by A1, PRE_TOPC:def_4; hence Down (V,B) is open by PRE_TOPC:def_2; ::_thesis: verum end; theorem Th29: :: CONNSP_3:29 for GX being non empty TopSpace for V, B being Subset of GX st V c= B holds Cl (Down (V,B)) = (Cl V) /\ B proof let GX be non empty TopSpace; ::_thesis: for V, B being Subset of GX st V c= B holds Cl (Down (V,B)) = (Cl V) /\ B let V, B be Subset of GX; ::_thesis: ( V c= B implies Cl (Down (V,B)) = (Cl V) /\ B ) assume V c= B ; ::_thesis: Cl (Down (V,B)) = (Cl V) /\ B then Down (V,B) = V by XBOOLE_1:28; then Cl (Down (V,B)) = (Cl V) /\ ([#] (GX | B)) by PRE_TOPC:17; hence Cl (Down (V,B)) = (Cl V) /\ B by PRE_TOPC:def_5; ::_thesis: verum end; theorem :: CONNSP_3:30 for GX being non empty TopSpace for B being Subset of GX for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B proof let GX be non empty TopSpace; ::_thesis: for B being Subset of GX for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B let B be Subset of GX; ::_thesis: for V being Subset of (GX | B) holds Cl V = (Cl (Up V)) /\ B let V be Subset of (GX | B); ::_thesis: Cl V = (Cl (Up V)) /\ B A1: B = [#] (GX | B) by PRE_TOPC:def_5; then Cl (Down ((Up V),B)) = (Cl (Up V)) /\ B by Th29; hence Cl V = (Cl (Up V)) /\ B by A1, XBOOLE_1:28; ::_thesis: verum end; theorem :: CONNSP_3:31 for GX being non empty TopSpace for V, B being Subset of GX st V c= B holds Cl (Down (V,B)) c= Cl V proof let GX be non empty TopSpace; ::_thesis: for V, B being Subset of GX st V c= B holds Cl (Down (V,B)) c= Cl V let V, B be Subset of GX; ::_thesis: ( V c= B implies Cl (Down (V,B)) c= Cl V ) assume V c= B ; ::_thesis: Cl (Down (V,B)) c= Cl V then Cl (Down (V,B)) = (Cl V) /\ B by Th29; hence Cl (Down (V,B)) c= Cl V by XBOOLE_1:17; ::_thesis: verum end; theorem :: CONNSP_3:32 for GX being non empty TopSpace for B being Subset of GX for V being Subset of (GX | B) st V c= B holds Down ((Up V),B) = V by XBOOLE_1:28; theorem :: CONNSP_3:33 for GX being non empty TopSpace for B being Subset of GX for p being Point of GX st p in B holds Component_of (p,B) is connected proof let GX be non empty TopSpace; ::_thesis: for B being Subset of GX for p being Point of GX st p in B holds Component_of (p,B) is connected let B be Subset of GX; ::_thesis: for p being Point of GX st p in B holds Component_of (p,B) is connected let p be Point of GX; ::_thesis: ( p in B implies Component_of (p,B) is connected ) assume A1: p in B ; ::_thesis: Component_of (p,B) is connected then reconsider B9 = B as non empty Subset of GX ; ( Component_of (Down (p,B9)) is connected & Component_of (p,B) = Component_of (Down (p,B)) ) by A1, Th27; hence Component_of (p,B) is connected by CONNSP_1:23; ::_thesis: verum end; registration let T be non empty TopSpace; cluster non empty for a_union_of_components of T; existence not for b1 being a_union_of_components of T holds b1 is empty proof reconsider A = [#] T as a_union_of_components of T by Th20; not A is empty ; hence not for b1 being a_union_of_components of T holds b1 is empty ; ::_thesis: verum end; end; theorem :: CONNSP_3:34 for T being non empty TopSpace for A being non empty a_union_of_components of T st A is connected holds A is a_component proof let T be non empty TopSpace; ::_thesis: for A being non empty a_union_of_components of T st A is connected holds A is a_component let A be non empty a_union_of_components of T; ::_thesis: ( A is connected implies A is a_component ) consider F being Subset-Family of T such that A1: for B being Subset of T st B in F holds B is a_component and A2: A = union F by Def2; consider X being set such that X <> {} and A3: X in F by A2, ORDERS_1:6; reconsider X = X as Subset of T by A3; assume A4: A is connected ; ::_thesis: A is a_component F = {X} proof thus F c= {X} :: according to XBOOLE_0:def_10 ::_thesis: {X} c= F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in {X} ) assume A5: x in F ; ::_thesis: x in {X} then reconsider Y = x as Subset of T ; A6: ( X is a_component & X c= A ) by A1, A2, A3, ZFMISC_1:74; ( Y is a_component & Y c= A ) by A1, A2, A5, ZFMISC_1:74; then Y = A by A4, CONNSP_1:def_5 .= X by A4, A6, CONNSP_1:def_5 ; hence x in {X} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {X} or x in F ) assume x in {X} ; ::_thesis: x in F hence x in F by A3, TARSKI:def_1; ::_thesis: verum end; then A = X by A2, ZFMISC_1:25; hence A is a_component by A1, A3; ::_thesis: verum end;