connsp_3.miz

    begin

    reserve x,X,X2,Y,Y2 for set;

    reserve GX for non empty TopSpace;

    reserve A2,B2 for Subset of GX;

    reserve B for Subset of GX;

    definition

      let GX be TopStruct, V be Subset of GX;

      :: CONNSP_3:def1

      func Component_of V -> Subset of GX means

      : Def1: ex F be Subset-Family of GX st (for A be Subset of GX holds A in F iff A is connected & V c= A) & ( union F) = it ;

      existence

      proof

        defpred P[ set] means ex A1 be Subset of GX st A1 = $1 & A1 is connected & V c= $1;

        consider F be Subset-Family of GX such that

         A1: for A be Subset of GX holds A in F iff P[A] from SUBSET_1:sch 3;

        take ( union F), F;

        thus for A be Subset of GX holds A in F iff A is connected & V c= A

        proof

          let A be Subset of GX;

          thus A in F implies A is connected & V c= A

          proof

            assume A in F;

            then ex A1 be Subset of GX st A1 = A & A1 is connected & V c= A by A1;

            hence thesis;

          end;

          thus thesis by A1;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let S,S9 be Subset of GX;

        assume that

         A2: ex F be Subset-Family of GX st (for A be Subset of GX holds A in F iff A is connected & V c= A) & ( union F) = S and

         A3: ex F9 be Subset-Family of GX st (for A be Subset of GX holds A in F9 iff A is connected & V c= A) & ( union F9) = S9;

        consider F be Subset-Family of GX such that

         A4: for A be Subset of GX holds A in F iff A is connected & V c= A and

         A5: ( union F) = S by A2;

        consider F9 be Subset-Family of GX such that

         A6: for A be Subset of GX holds A in F9 iff A is connected & V c= A and

         A7: ( union F9) = S9 by A3;

        now

          let y be object;

           A8:

          now

            assume y in S9;

            then

            consider B be set such that

             A9: y in B and

             A10: B in F9 by A7, TARSKI:def 4;

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

          end;

          now

            assume y in S;

            then

            consider B be set such that

             A11: y in B and

             A12: B in F by A5, TARSKI:def 4;

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

          end;

          hence y in S iff y in S9 by A8;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: CONNSP_3:1



     Th1: for GX be TopSpace, V be Subset of GX st (ex A be Subset of GX st A is connected & V c= A) holds V c= ( Component_of V)

    proof

      let GX be TopSpace, V be Subset of GX;

      given A be Subset of GX such that

       A1: A is connected & V c= A;

      consider F be Subset-Family of GX such that

       A2: for A be 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 be set holds A in F implies 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 thesis by A3, A5;

    end;

    theorem :: CONNSP_3:2

    for GX be TopSpace, V be Subset of GX st ( not ex A be Subset of GX st A is connected & V c= A) holds ( Component_of V) = {}

    proof

      let GX be TopSpace, V be Subset of GX such that

       A1: not ex A be Subset of GX st A is connected & V c= A;

      consider F be Subset-Family of GX such that

       A2: for A be Subset of GX holds A in F iff A is connected & V c= A and

       A3: ( Component_of V) = ( union F) by Def1;

      now

        assume F <> {} ;

        then

        consider A be Subset of GX such that

         A4: A in F by SUBSET_1: 4;

        reconsider A as Subset of GX;

        A is connected & V c= A by A2, A4;

        hence contradiction by A1;

      end;

      hence thesis by A3, ZFMISC_1: 2;

    end;

    theorem :: CONNSP_3:3



     Th3: ( Component_of ( {} GX)) = the carrier of GX

    proof

      defpred P[ set] means ex A1 be Subset of GX st A1 = $1 & A1 is connected & ( {} GX) c= $1;

      consider F be Subset-Family of GX such that

       A1: for A be Subset of GX holds A in F iff P[A] from SUBSET_1:sch 3;



       A2: for A be Subset of GX holds A in F iff A is connected & ( {} GX) c= A

      proof

        let A be Subset of GX;

        thus A in F implies A is connected & ( {} GX) c= A

        proof

          assume A in F;

          then ex A1 be Subset of GX st A1 = A & A1 is connected & ( {} GX) c= A by A1;

          hence thesis;

        end;

        thus thesis by A1;

      end;

      now

        let x be object;

        hereby

          assume x in the carrier of GX;

          then

          reconsider p = x as Point of GX;

          reconsider Y = ( Component_of p) as set;

          take Y;

          thus x in Y by CONNSP_1: 38;

          ( Component_of p) is connected & ( {} GX) c= Y;

          hence Y in F by A2;

        end;

        given Y be set such that

         A3: x in Y & Y in F;

        thus x in the carrier of GX by A3;

      end;

      then ( union F) = the carrier of GX by TARSKI:def 4;

      hence thesis by A2, Def1;

    end;

    theorem :: CONNSP_3:4

    for V be Subset of GX st V is connected holds ( Component_of V) <> {}

    proof

      let V be Subset of GX such that

       A1: V is connected;

      per cases ;

        suppose V = {} ;

        then V = ( {} GX);

        hence thesis by Th3;

      end;

        suppose V <> {} ;

        hence thesis by A1, Th1, XBOOLE_1: 3;

      end;

    end;

    theorem :: CONNSP_3:5



     Th5: for GX be TopSpace, V be Subset of GX st V is connected & V <> {} holds ( Component_of V) is connected

    proof

      let GX be TopSpace;

      let V be Subset of GX;

      assume that

       A1: V is connected and

       A2: V <> {} ;

      consider F be Subset-Family of GX such that

       A3: for A be 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 be 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 be Subset of GX st A in F holds A is connected by A3;

      hence thesis by A4, A6, CONNSP_1: 26;

    end;

    theorem :: CONNSP_3:6



     Th6: for V,C be Subset of GX st V is connected & C is connected holds ( Component_of V) c= C implies C = ( Component_of V)

    proof

      let V,C be Subset of GX;

      assume that

       A1: V is connected and

       A2: C is connected;

      assume

       A3: ( Component_of V) c= C;

      consider F be Subset-Family of GX such that

       A4: for A be 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;

      then C in F by A2, A4;

      then C c= ( Component_of V) by A5, ZFMISC_1: 74;

      hence thesis by A3;

    end;

    theorem :: CONNSP_3:7



     Th7: for A be Subset of GX st A is a_component holds ( Component_of A) = A

    proof

      let A be Subset of GX;

      assume

       A1: A is a_component;

      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 thesis by A1, A3, CONNSP_1:def 5;

    end;

    theorem :: CONNSP_3:8



     Th8: for A be Subset of GX holds A is a_component iff ex V be Subset of GX st V is connected & V <> {} & A = ( Component_of V)

    proof

      let A be Subset of GX;

       A1:

      now

        assume

         A2: A is a_component;

        take V = A;

        thus V is connected & V <> {} & A = ( Component_of V) by A2, Th7;

      end;

      now

        given V be Subset of GX such that

         A3: V is connected & V <> {} & A = ( Component_of V);

        A is connected & for B be Subset of GX st B is connected holds A c= B implies A = B by A3, Th5, Th6;

        hence A is a_component by CONNSP_1:def 5;

      end;

      hence thesis by A1;

    end;

    theorem :: CONNSP_3:9

    for V be Subset of GX st V is connected & V <> {} holds ( Component_of V) is a_component by Th8;

    theorem :: CONNSP_3:10

    for A,V be Subset of GX st A is a_component & V is connected & V c= A & V <> {} holds A = ( Component_of V)

    proof

      let A,V be Subset of GX;

      assume that

       A1: A is a_component and

       A2: V is connected and

       A3: V c= A and

       A4: 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);

      ( Component_of V) is a_component by A2, A4, Th8;

      hence contradiction by A1, A6, A5, CONNSP_1: 1, CONNSP_1: 34;

    end;

    theorem :: CONNSP_3:11



     Th11: for V be Subset of GX st V is connected & V <> {} holds ( Component_of ( Component_of V)) = ( Component_of V)

    proof

      let V be Subset of GX;

      assume V is connected & V <> {} ;

      then ( Component_of V) is a_component by Th8;

      hence thesis by Th7;

    end;

    theorem :: CONNSP_3:12



     Th12: for A,B be Subset of GX st A is connected & B is connected & A <> {} & A c= B holds ( Component_of A) = ( Component_of B)

    proof

      let A,B be Subset of GX;

      assume that

       A1: A is connected and

       A2: B is connected and

       A3: A <> {} and

       A4: A c= 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;



       A8: ( Component_of B) c= ( Component_of A)

      proof

        consider F be Subset-Family of GX such that

         A9: for D be 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 thesis by A10, ZFMISC_1: 74;

      end;



       A11: ( Component_of A) is connected by A1, A3, Th5;

      ( Component_of A) c= ( Component_of B)

      proof

        consider F be Subset-Family of GX such that

         A12: for D be 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;

        then ( Component_of A) in F by A11, A12;

        hence thesis by A13, ZFMISC_1: 74;

      end;

      hence thesis by A8;

    end;

    theorem :: CONNSP_3:13



     Th13: for A,B be Subset of GX st A is connected & B is connected & A <> {} & A c= B holds B c= ( Component_of A)

    proof

      let A,B be Subset of GX;

      assume that

       A1: A is connected and

       A2: B is connected and

       A3: A <> {} & A c= B;

      ( Component_of A) = ( Component_of B) by A1, A2, A3, Th12;

      hence thesis by A2, Th1;

    end;

    theorem :: CONNSP_3:14



     Th14: for A be Subset of GX, B be Subset of GX st A is connected & (A \/ B) is connected & A <> {} holds (A \/ B) c= ( Component_of A)

    proof

      let A be Subset of GX, B be Subset of GX;

      assume that

       A1: A is connected and

       A2: (A \/ B) is connected and

       A3: A <> {} ;

      ( Component_of (A \/ B)) = ( Component_of A) by A1, A2, A3, Th12, XBOOLE_1: 7;

      hence thesis by A2, Th1;

    end;

    theorem :: CONNSP_3:15



     Th15: for A be Subset of GX, p be Point of GX st A is connected & p in A holds ( Component_of p) = ( Component_of A)

    proof

      let A be Subset of GX, p be Point of GX;

      assume that

       A1: A is connected and

       A2: p in A;

      A c= ( Component_of A) & ( Component_of A) is a_component by A1, A2, Th1, Th8;

      hence thesis by A2, CONNSP_1: 41;

    end;

    theorem :: CONNSP_3:16

    for A,B be 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 A,B be Subset of GX;



       A1: A c= (A \/ B) & B c= (A \/ B) by XBOOLE_1: 7;



       A2: for C,D be 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;

        assume that

         A3: C is connected and

         A4: D is connected and

         A5: (C /\ D) <> {} ;

        C meets D by A5;

        then

         A6: (C \/ D) is connected by A3, A4, CONNSP_1: 1, CONNSP_1: 17;

        C <> {} by A5;

        hence thesis by A3, A6, Th14;

      end;

      assume A is connected & B is connected & (A /\ B) <> {} ;

      then (A \/ B) c= ( Component_of A) & (A \/ B) c= ( Component_of B) by A2;

      hence thesis by A1;

    end;

    theorem :: CONNSP_3:17

    for A be Subset of GX st A is connected & A <> {} holds ( Cl A) c= ( Component_of A)

    proof

      let A be Subset of GX;

      assume that

       A1: A is connected and

       A2: A <> {} ;

      ( Cl A) is connected by A1, CONNSP_1: 19;

      hence thesis by A1, A2, Th13, PRE_TOPC: 18;

    end;

    theorem :: CONNSP_3:18

    for A,B be Subset of GX st A is a_component & B is connected & B <> {} & A misses B holds A misses ( Component_of B)

    proof

      let A,B be Subset of GX;

      assume that

       A1: A is a_component and

       A2: B is connected & B <> {} and

       A3: (A /\ B) = {} ;



       A4: A is connected by A1;

      assume (A /\ ( Component_of B)) <> {} ;

      then

      consider x be 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;

    end;

    begin

     Lm1:

    now

      let GX be TopStruct;

      reconsider S = {} as Subset-Family of GX by XBOOLE_1: 2;

      for B be Subset of GX st B in S holds B is a_component;

      hence ex F be Subset-Family of GX st (for B be Subset of GX st B in F holds B is a_component) & ( {} GX) = ( union F) by ZFMISC_1: 2;

    end;

    definition

      let GX be TopStruct;

      :: CONNSP_3:def2

      mode a_union_of_components of GX -> Subset of GX means

      : Def2: ex F be Subset-Family of GX st (for B be Subset of GX st B in F holds B is a_component) & it = ( union F);

      existence

      proof

        take ( {} GX);

        thus thesis by Lm1;

      end;

    end

    theorem :: CONNSP_3:19



     Th19: ( {} GX) is a_union_of_components of GX

    proof

      thus ex F be Subset-Family of GX st (for B be Subset of GX st B in F holds B is a_component) & ( {} GX) = ( union F) by Lm1;

    end;

    theorem :: CONNSP_3:20



     Th20: for A be Subset of GX st A = the carrier of GX holds A is a_union_of_components of GX

    proof

      let A be Subset of GX;

      { B : B is a_component } c= ( bool the carrier of GX)

      proof

        let x be object;

        assume x in { B : B is a_component };

        then ex B be Subset of GX st x = B & B is a_component;

        hence thesis;

      end;

      then

      reconsider S = { B : B is a_component } as Subset-Family of GX;



       A1: for B be Subset of GX st B in S holds B is a_component

      proof

        let B be Subset of GX;

        assume B in S;

        then ex B2 be Subset of GX st B = B2 & B2 is a_component;

        hence thesis;

      end;

      the carrier of GX c= ( union S)

      proof

        let x be object;

        assume x in the carrier of GX;

        then

        reconsider p = x as Point of GX;

        set B3 = ( Component_of p);

        B3 is a_component by CONNSP_1: 40;

        then p in ( Component_of p) & B3 in S by CONNSP_1: 38;

        hence thesis by TARSKI:def 4;

      end;

      then

       A2: the carrier of GX = ( union S);

      assume A = the carrier of GX;

      hence thesis by A2, A1, Def2;

    end;

    theorem :: CONNSP_3:21



     Th21: for A be Subset of GX, p be Point of GX st p in A & A is a_union_of_components of GX holds ( Component_of p) c= A

    proof

      let A be Subset of GX, p be Point of GX;

      assume that

       A1: p in A and

       A2: A is a_union_of_components of GX;

      consider F be Subset-Family of GX such that

       A3: for B be Subset of GX st B in F holds B is a_component and

       A4: A = ( union F) by A2, Def2;

      consider X 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 thesis by A4, A6, ZFMISC_1: 74;

    end;

    theorem :: CONNSP_3:22

    for A,B be 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 A,B be Subset of GX;

      assume that

       A1: A is a_union_of_components of GX and

       A2: B is a_union_of_components of GX;

      consider Fa be Subset-Family of GX such that

       A3: for Ba be Subset of GX st Ba in Fa holds Ba is a_component and

       A4: A = ( union Fa) by A1, Def2;

      consider Fb be Subset-Family of GX such that

       A5: for Bb be Subset of GX st Bb in Fb holds Bb is a_component and

       A6: B = ( union Fb) by A2, Def2;



       A7: for B2 be Subset of GX st B2 in (Fa \/ Fb) holds B2 is a_component

      proof

        let B2 be Subset of GX;

        assume B2 in (Fa \/ Fb);

        then B2 in Fa or B2 in Fb by XBOOLE_0:def 3;

        hence thesis by A3, A5;

      end;



       A8: (A /\ B) is a_union_of_components of GX

      proof

        reconsider Fd = (Fa /\ Fb) as Subset-Family of GX;



         A9: for B4 be Subset of GX st B4 in Fd holds B4 is a_component

        proof

          let B4 be Subset of GX;

          assume B4 in Fd;

          then B4 in Fa by XBOOLE_0:def 4;

          hence thesis by A3;

        end;



         A10: (A /\ B) c= ( union Fd)

        proof

          let x be object;

          assume

           A11: x in (A /\ B);

          then x in A by XBOOLE_0:def 4;

          then

          consider F1 be 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 be 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;

          hence thesis by A12, TARSKI:def 4;

        end;

        ( union Fd) c= (A /\ B)

        proof

          let x be object;

          assume x in ( union Fd);

          then

          consider X4 be 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 thesis by A4, A6, A20, XBOOLE_0:def 4;

        end;

        then (A /\ B) = ( union Fd) by A10;

        hence thesis by A9, Def2;

      end;

      reconsider Fc = (Fa \/ Fb) as Subset-Family of GX;

      (A \/ B) = ( union Fc) by A4, A6, ZFMISC_1: 78;

      hence thesis by A7, A8, Def2;

    end;

    theorem :: CONNSP_3:23

    for Fu be Subset-Family of GX st (for A be 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 Fu be Subset-Family of GX;

      { B : ex B2 st B2 in Fu & B c= B2 & B is a_component } c= ( bool the carrier of GX)

      proof

        let x be object;

        assume x in { B : ex B2 st B2 in Fu & B c= B2 & B is a_component };

        then ex B st x = B & ex B2 st B2 in Fu & B c= B2 & B is a_component;

        hence thesis;

      end;

      then

      reconsider F2 = { B : ex B2 st B2 in Fu & B c= B2 & B is a_component } as Subset-Family of GX;



       A1: for B be Subset of GX st B in F2 holds B is a_component

      proof

        let B be Subset of GX;

        assume B in F2;

        then ex A2 be Subset of GX st B = A2 & ex B2 st B2 in Fu & A2 c= B2 & A2 is a_component;

        hence thesis;

      end;

      assume

       A2: for A be Subset of GX st A in Fu holds A is a_union_of_components of GX;



       A3: ( union Fu) c= ( union F2)

      proof

        let x be object;

        assume x in ( union Fu);

        then

        consider X2 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 be Subset-Family of GX such that

         A6: for B be Subset of GX st B in F holds B is a_component and

         A7: B3 = ( union F) by Def2;

        consider Y2 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 thesis by A8, TARSKI:def 4;

      end;

      ( union F2) c= ( union Fu)

      proof

        let x be object;

        assume x in ( union F2);

        then

        consider X such that

         A10: x in X and

         A11: X in F2 by TARSKI:def 4;

        ex B st X = B & ex B2 st B2 in Fu & B c= B2 & B is a_component by A11;

        hence thesis by A10, TARSKI:def 4;

      end;

      then ( union Fu) = ( union F2) by A3;

      hence thesis by A1, Def2;

    end;

    theorem :: CONNSP_3:24

    for Fu be Subset-Family of GX st (for A be 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 Fu be Subset-Family of GX;

      assume

       A1: for A be Subset of GX st A in Fu holds A is a_union_of_components of GX;

      now

        per cases ;

          case

           A2: Fu <> {} ;

          { B : B is a_component & for A2 st A2 in Fu holds B c= A2 } c= ( bool the carrier of GX)

          proof

            let x be object;

            assume x in { B : B is a_component & for A2 st A2 in Fu holds B c= A2 };

            then ex B st x = B & B is a_component & for A2 st A2 in Fu holds B c= A2;

            hence thesis;

          end;

          then

          reconsider F1 = { B : B is a_component & for A2 st A2 in Fu holds B c= A2 } as Subset-Family of GX;



           A3: ( meet Fu) c= ( union F1)

          proof

            let x be object;

            consider Y2 be object such that

             A4: Y2 in Fu by A2, XBOOLE_0:def 1;

            reconsider Y2 as set by TARSKI: 1;

            reconsider B2 = Y2 as Subset of GX by A4;

            B2 is a_union_of_components of GX by A1, A4;

            then

            consider F be Subset-Family of GX such that

             A5: for B be 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);

            then x in Y2 by A4, SETFAM_1:def 1;

            then

            consider Y3 be 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 st A2 in Fu holds B3 c= A2

            proof

              reconsider p = x as Point of GX by A7;

              let A2;

              assume

               A11: A2 in Fu;

              then x in A2 by A7, SETFAM_1:def 1;

              then ( Component_of p) c= A2 by A1, A11, Th21;

              hence thesis by A5, A8, A9, CONNSP_1: 41;

            end;

            B3 is a_component by A5, A9;

            then Y3 in F1 by A10;

            hence thesis by A8, TARSKI:def 4;

          end;



           A12: for B be Subset of GX st B in F1 holds B is a_component

          proof

            let B be Subset of GX;

            assume B in F1;

            then ex B1 be Subset of GX st B = B1 & B1 is a_component & for A2 st A2 in Fu holds B1 c= A2;

            hence thesis;

          end;

          ( union F1) c= ( meet Fu)

          proof

            let x be object;

            assume x in ( union F1);

            then

            consider X such that

             A13: x in X and

             A14: X in F1 by TARSKI:def 4;

            consider B such that

             A15: X = B and B is a_component and

             A16: for A2 st A2 in Fu holds B c= A2 by A14;

            for Y st Y in Fu holds x in Y

            proof

              let Y;

              assume Y in Fu;

              then B c= Y by A16;

              hence thesis by A13, A15;

            end;

            hence thesis by A2, SETFAM_1:def 1;

          end;

          then ( meet Fu) = ( union F1) by A3;

          hence thesis by A12, Def2;

        end;

          case Fu = {} ;

          then ( meet Fu) = ( {} GX) by SETFAM_1:def 1;

          hence thesis by Th19;

        end;

      end;

      hence thesis;

    end;

    theorem :: CONNSP_3:25

    for A,B be 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 A,B be Subset of GX;

      assume that

       A1: A is a_union_of_components of GX and

       A2: B is a_union_of_components of GX;

      consider Fa be Subset-Family of GX such that

       A3: for B2 be Subset of GX st B2 in Fa holds B2 is a_component and

       A4: A = ( union Fa) by A1, Def2;

      consider Fb be Subset-Family of GX such that

       A5: for B3 be 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 object;

        assume x in ( union Fd);

        then

        consider X 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

          assume x in B;

          then

          consider Y3 be 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;

          B3 is a_component by A5, A15;

          hence contradiction by A10, A12, A15, A16, CONNSP_1: 35;

        end;

        A2 c= A by A4, A11, ZFMISC_1: 74;

        hence thesis by A8, A13, XBOOLE_0:def 5;

      end;



       A17: for B4 be Subset of GX st B4 in Fd holds B4 is a_component

      proof

        let B4 be Subset of GX;

        assume B4 in Fd;

        then B4 in Fa by XBOOLE_0:def 5;

        hence thesis by A3;

      end;

      (A \ B) c= ( union Fd)

      proof

        let x be object;

        assume

         A18: x in (A \ B);

        then x in A by XBOOLE_0:def 5;

        then

        consider X 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

          assume A2 in Fb;

          then A2 c= B by A6, ZFMISC_1: 74;

          hence contradiction by A18, A19, XBOOLE_0:def 5;

        end;

        then A2 in Fd by A20, XBOOLE_0:def 5;

        hence thesis by A19, TARSKI:def 4;

      end;

      then (A \ B) = ( union Fd) by A7;

      hence thesis by A17, Def2;

    end;

    begin

    definition

      let GX be TopStruct, B be Subset of GX, p be Point of GX;

      assume

       A1: p in B;

      :: CONNSP_3:def3

      func Down (p,B) -> Point of (GX | B) equals

      : Def3: p;

      coherence

      proof

        B = ( [#] (GX | B)) by PRE_TOPC:def 5;

        hence thesis by A1;

      end;

    end

    definition

      let GX be TopStruct, B be Subset of GX, p be Point of (GX | B);

      assume

       A1: B <> {} ;

      :: CONNSP_3:def4

      func Up (p) -> Point of GX equals p;

      coherence

      proof

        B = the carrier of (GX | B) by PRE_TOPC: 8;

        then p in B by A1;

        hence thesis;

      end;

    end

    definition

      let GX be TopStruct, V,B be Subset of GX;

      :: CONNSP_3:def5

      func Down (V,B) -> Subset of (GX | B) equals (V /\ B);

      coherence

      proof

        B = ( [#] (GX | B)) by PRE_TOPC:def 5;

        hence thesis by XBOOLE_1: 17;

      end;

    end

    definition

      let GX be TopStruct, B be Subset of GX;

      let V be Subset of (GX | B);

      :: CONNSP_3:def6

      func Up (V) -> Subset of GX equals V;

      coherence

      proof

        B = the carrier of (GX | B) by PRE_TOPC: 8;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    definition

      let GX be TopStruct, B be Subset of GX, p be Point of GX;

      assume

       A1: p in B;

      :: CONNSP_3:def7

      func Component_of (p,B) -> Subset of GX means

      : Def7: for q be Point of (GX | B) st q = p holds it = ( Component_of q);

      existence

      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;

        thus thesis;

      end;

      uniqueness

      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;

        assume that

         A3: for q be Point of (GX | B) st q = p holds S = ( Component_of q) and

         A4: for q2 be Point of (GX | B) st q2 = p holds S9 = ( Component_of q2);

        S = ( Component_of q3) by A3;

        hence thesis by A4;

      end;

    end

    theorem :: CONNSP_3:26

    for B be Subset of GX, p be Point of GX st p in B holds p in ( Component_of (p,B))

    proof

      let B be Subset of GX, p be Point of GX;

      assume

       A1: p in 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 thesis by A1, Def7;

    end;

    theorem :: CONNSP_3:27



     Th27: for B be Subset of GX, p be Point of GX st p in B holds ( Component_of (p,B)) = ( Component_of ( Down (p,B)))

    proof

      let B be Subset of GX, p be Point of GX;

      assume

       A1: p in B;

      then p = ( Down (p,B)) by Def3;

      hence thesis by A1, Def7;

    end;

    theorem :: CONNSP_3:28

    for GX be TopSpace holds for V,B be Subset of GX st V is open holds ( Down (V,B)) is open

    proof

      let GX be TopSpace;

      let V,B be Subset of GX;

      assume V 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 thesis by PRE_TOPC:def 2;

    end;

    theorem :: CONNSP_3:29



     Th29: for V,B be Subset of GX st V c= B holds ( Cl ( Down (V,B))) = (( Cl V) /\ B)

    proof

      let V,B be Subset of GX;

      assume V c= B;

      then ( Down (V,B)) = V by XBOOLE_1: 28;

      then ( Cl ( Down (V,B))) = (( Cl V) /\ ( [#] (GX | B))) by PRE_TOPC: 17;

      hence thesis by PRE_TOPC:def 5;

    end;

    theorem :: CONNSP_3:30

    for B be Subset of GX, V be Subset of (GX | B) holds ( Cl V) = (( Cl ( Up V)) /\ B)

    proof

      let B be Subset of GX, V be Subset of (GX | B);



       A1: B = ( [#] (GX | B)) by PRE_TOPC:def 5;

      then ( Cl ( Down (( Up V),B))) = (( Cl ( Up V)) /\ B) by Th29;

      hence thesis by A1, XBOOLE_1: 28;

    end;

    theorem :: CONNSP_3:31

    for V,B be Subset of GX st V c= B holds ( Cl ( Down (V,B))) c= ( Cl V)

    proof

      let V,B be Subset of GX;

      assume V c= B;

      then ( Cl ( Down (V,B))) = (( Cl V) /\ B) by Th29;

      hence thesis by XBOOLE_1: 17;

    end;

    theorem :: CONNSP_3:32

    for B be Subset of GX, V be Subset of (GX | B) st V c= B holds ( Down (( Up V),B)) = V by XBOOLE_1: 28;

    theorem :: CONNSP_3:33

    for B be Subset of GX, p be Point of GX st p in B holds ( Component_of (p,B)) is connected

    proof

      let B be Subset of GX, p be Point of GX;

      assume

       A1: p in B;

      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 thesis by CONNSP_1: 23;

    end;

    registration

      let T be non empty TopSpace;

      cluster non empty for a_union_of_components of T;

      existence

      proof

        reconsider A = ( [#] T) as a_union_of_components of T by Th20;

        A is non empty;

        hence thesis;

      end;

    end

    theorem :: CONNSP_3:34

    for T be non empty TopSpace holds for A be non empty a_union_of_components of T st A is connected holds A is a_component

    proof

      let T be non empty TopSpace;

      let A be non empty a_union_of_components of T;

      consider F be Subset-Family of T such that

       A1: for B be Subset of T st B in F holds B is a_component and

       A2: A = ( union F) by Def2;

      consider X be set such that X <> {} and

       A3: X in F by A2, ORDERS_1: 6;

      reconsider X as Subset of T by A3;

      assume

       A4: A is connected;

      F = {X}

      proof

        thus F c= {X}

        proof

          let x be object;

          assume

           A5: x in F;

          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 thesis by TARSKI:def 1;

        end;

        let x be object;

        assume x in {X};

        hence thesis by A3, TARSKI:def 1;

      end;

      then A = X by A2, ZFMISC_1: 25;

      hence thesis by A1, A3;

    end;