connsp_2.miz

    begin

    definition

      let X be non empty TopSpace, x be Point of X;

      :: CONNSP_2:def1

      mode a_neighborhood of x -> Subset of X means

      : Def1: x in ( Int it );

      existence

      proof

        take ( [#] X);

        ( Int ( [#] X)) = ( [#] X) by TOPS_1: 15;

        hence thesis;

      end;

    end

    definition

      let X be TopSpace, A be Subset of X;

      :: CONNSP_2:def2

      mode a_neighborhood of A -> Subset of X means

      : Def2: A c= ( Int it );

      existence

      proof

        take ( [#] X);

        ( Int ( [#] X)) = ( [#] X) by TOPS_1: 15;

        hence thesis;

      end;

    end

    reserve X for non empty TopSpace;

    reserve x for Point of X;

    reserve U1 for Subset of X;

    theorem :: CONNSP_2:1

    for A,B be Subset of X holds A is a_neighborhood of x & B is a_neighborhood of x implies (A \/ B) is a_neighborhood of x

    proof

      let A,B be Subset of X;

      reconsider A1 = A, B1 = B as Subset of X;

      A1 is a_neighborhood of x & B1 is a_neighborhood of x implies (A1 \/ B1) is a_neighborhood of x

      proof

        assume that

         A1: x in ( Int A1) and x in ( Int B1);



         A2: (( Int A1) \/ ( Int B1)) c= ( Int (A1 \/ B1)) by TOPS_1: 20;

        x in (( Int A1) \/ ( Int B1)) by A1, XBOOLE_0:def 3;

        hence thesis by A2, Def1;

      end;

      hence thesis;

    end;

    theorem :: CONNSP_2:2

    for A,B be Subset of X holds A is a_neighborhood of x & B is a_neighborhood of x iff (A /\ B) is a_neighborhood of x

    proof

      let A,B be Subset of X;

      A is a_neighborhood of x & B is a_neighborhood of x iff x in ( Int A) & x in ( Int B) by Def1;

      then A is a_neighborhood of x & B is a_neighborhood of x iff x in (( Int A) /\ ( Int B)) by XBOOLE_0:def 4;

      then A is a_neighborhood of x & B is a_neighborhood of x iff x in ( Int (A /\ B)) by TOPS_1: 17;

      hence thesis by Def1;

    end;

    theorem :: CONNSP_2:3



     Th3: for U1 be Subset of X, x be Point of X st U1 is open & x in U1 holds U1 is a_neighborhood of x

    proof

      let U1 be Subset of X, x be Point of X;

      assume U1 is open & x in U1;

      then x in ( Int U1) by TOPS_1: 23;

      hence thesis by Def1;

    end;

    theorem :: CONNSP_2:4



     Th4: for U1 be Subset of X, x be Point of X st U1 is a_neighborhood of x holds x in U1

    proof

      let U1 be Subset of X, x be Point of X;

      assume U1 is a_neighborhood of x;

      then

       A1: x in ( Int U1) by Def1;

      ( Int U1) c= U1 by TOPS_1: 16;

      hence thesis by A1;

    end;

    theorem :: CONNSP_2:5



     Th5: U1 is a_neighborhood of x implies ex V be non empty Subset of X st V is a_neighborhood of x & V is open & V c= U1

    proof

      assume U1 is a_neighborhood of x;

      then x in ( Int U1) by Def1;

      then

      consider V be Subset of X such that

       A1: V is open & V c= U1 and

       A2: x in V by TOPS_1: 22;

      reconsider V as non empty Subset of X by A2;

      take V;

      thus thesis by A1, A2, Th3;

    end;

    theorem :: CONNSP_2:6



     Th6: U1 is a_neighborhood of x iff ex V be Subset of X st V is open & V c= U1 & x in V

    proof

       A1:

      now

        assume U1 is a_neighborhood of x;

        then

        consider V be non empty Subset of X such that

         A2: V is a_neighborhood of x & V is open & V c= U1 by Th5;

        take V;

        thus ex V be Subset of X st V is open & V c= U1 & x in V by A2, Th4;

      end;

      now

        given V be Subset of X such that

         A3: V is open & V c= U1 & x in V;

        x in ( Int U1) by A3, TOPS_1: 22;

        hence U1 is a_neighborhood of x by Def1;

      end;

      hence thesis by A1;

    end;

    theorem :: CONNSP_2:7

    for U1 be Subset of X holds U1 is open iff for x st x in U1 holds ex A be Subset of X st A is a_neighborhood of x & A c= U1

    proof

      let U1 be Subset of X;

      now

        assume

         A1: for x st x in U1 holds ex A be Subset of X st A is a_neighborhood of x & A c= U1;

        for x be set holds x in U1 iff ex V be Subset of X st V is open & V c= U1 & x in V

        proof

          let x be set;

          thus x in U1 implies ex V be Subset of X st V is open & V c= U1 & x in V

          proof

            assume

             A2: x in U1;

            then

            reconsider x as Point of X;

            consider S be Subset of X such that

             A3: S is a_neighborhood of x and

             A4: S c= U1 by A1, A2;

            consider V be Subset of X such that

             A5: V is open & V c= S & x in V by A3, Th6;

            take V;

            thus thesis by A4, A5;

          end;

          given V be Subset of X such that V is open and

           A6: V c= U1 & x in V;

          thus thesis by A6;

        end;

        hence U1 is open by TOPS_1: 25;

      end;

      hence thesis by Th3;

    end;

    theorem :: CONNSP_2:8

    for V be Subset of X holds V is a_neighborhood of {x} iff V is a_neighborhood of x

    proof

      let V be Subset of X;

      thus V is a_neighborhood of {x} implies V is a_neighborhood of x

      proof

        assume V is a_neighborhood of {x};

        then

         A1: {x} c= ( Int V) by Def2;

        x in {x} by TARSKI:def 1;

        hence thesis by A1, Def1;

      end;

      assume V is a_neighborhood of x;

      then x in ( Int V) by Def1;

      then for p be object holds p in {x} implies p in ( Int V) by TARSKI:def 1;

      then {x} c= ( Int V);

      hence thesis by Def2;

    end;

    theorem :: CONNSP_2:9



     Th9: for B be non empty Subset of X, x be Point of (X | B), A be Subset of (X | B), A1 be Subset of X, x1 be Point of X st B is open & A is a_neighborhood of x & A = A1 & x = x1 holds A1 is a_neighborhood of x1

    proof

      let B be non empty Subset of X, x be Point of (X | B), A be Subset of (X | B), A1 be Subset of X, x1 be Point of X such that

       A1: B is open and

       A2: A is a_neighborhood of x and

       A3: A = A1 & x = x1;

      x in ( Int A) by A2, Def1;

      then

      consider Q1 be Subset of (X | B) such that

       A4: Q1 is open and

       A5: Q1 c= A & x in Q1 by TOPS_1: 22;

      Q1 in the topology of (X | B) by A4, PRE_TOPC:def 2;

      then

      consider Q be Subset of X such that

       A6: Q in the topology of X and

       A7: Q1 = (Q /\ ( [#] (X | B))) by PRE_TOPC:def 4;

      reconsider Q2 = Q as Subset of X;

      Q2 is open by A6, PRE_TOPC:def 2;

      then

       A8: (Q /\ B) is open by A1;

      Q1 = (Q /\ B) by A7, PRE_TOPC:def 5;

      then x1 in ( Int A1) by A3, A5, A8, TOPS_1: 22;

      hence thesis by Def1;

    end;



     Lm1: for X1 be SubSpace of X, A be Subset of X, A1 be Subset of X1 st A = A1 holds (( Int A) /\ ( [#] X1)) c= ( Int A1)

    proof

      let X1 be SubSpace of X, A be Subset of X, A1 be Subset of X1;

      assume

       A1: A = A1;

      let p be object;

      assume

       A2: p in (( Int A) /\ ( [#] X1));

      then p in ( Int A) by XBOOLE_0:def 4;

      then

      consider Q be Subset of X such that

       A3: Q is open and

       A4: Q c= A & p in Q by TOPS_1: 22;

      ex Q1 be Subset of X1 st Q1 is open & Q1 c= A1 & p in Q1

      proof

        reconsider Q1 = (Q /\ ( [#] X1)) as Subset of X1;

        take Q1;

        Q in the topology of X by A3, PRE_TOPC:def 2;

        then Q1 c= Q & Q1 in the topology of X1 by PRE_TOPC:def 4, XBOOLE_1: 17;

        hence thesis by A1, A2, A4, PRE_TOPC:def 2, XBOOLE_0:def 4;

      end;

      hence thesis by TOPS_1: 22;

    end;

    theorem :: CONNSP_2:10



     Th10: for B be non empty Subset of X, x be Point of (X | B), A be Subset of (X | B), A1 be Subset of X, x1 be Point of X st A1 is a_neighborhood of x1 & A = A1 & x = x1 holds A is a_neighborhood of x

    proof

      let B be non empty Subset of X, x be Point of (X | B), A be Subset of (X | B), A1 be Subset of X, x1 be Point of X such that

       A1: A1 is a_neighborhood of x1 and

       A2: A = A1 and

       A3: x = x1;

      x1 in ( Int A1) by A1, Def1;

      then

       A4: x1 in (( Int A1) /\ ( [#] (X | B))) by A3, XBOOLE_0:def 4;

      (( Int A1) /\ ( [#] (X | B))) c= ( Int A) by A2, Lm1;

      hence thesis by A3, A4, Def1;

    end;

    theorem :: CONNSP_2:11



     Th11: for A be Subset of X, B be Subset of X st A is a_component & A c= B holds A is_a_component_of B

    proof

      let A be Subset of X, B be Subset of X such that

       A1: A is a_component and

       A2: A c= B;



       A3: A is connected by A1;

      ex A1 be Subset of (X | B) st A = A1 & A1 is a_component

      proof

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

        then

        reconsider C = A as Subset of (X | B) by A2;

        take A1 = C;



         A4: for D be Subset of (X | B) st D is connected holds A1 c= D implies A1 = D

        proof

          let D be Subset of (X | B) such that

           A5: D is connected;

          reconsider D1 = D as Subset of X by PRE_TOPC: 11;

          assume

           A6: A1 c= D;

          D1 is connected by A5, CONNSP_1: 23;

          hence thesis by A1, A6, CONNSP_1:def 5;

        end;

        A1 is connected by A3, CONNSP_1: 23;

        hence thesis by A4, CONNSP_1:def 5;

      end;

      hence thesis by CONNSP_1:def 6;

    end;

    theorem :: CONNSP_2:12

    for X1 be non empty SubSpace of X, x be Point of X, x1 be Point of X1 st x = x1 holds ( Component_of x1) c= ( Component_of x)

    proof

      let X1 be non empty SubSpace of X, x be Point of X, x1 be Point of X1;

      consider F be Subset-Family of X such that

       A1: for A be Subset of X holds A in F iff A is connected & x in A and

       A2: ( union F) = ( Component_of x) by CONNSP_1:def 7;

      reconsider Z = ( Component_of x1) as Subset of X by PRE_TOPC: 11;



       A3: x1 in Z & Z is connected by CONNSP_1: 23, CONNSP_1: 38;

      assume x = x1;

      then Z in F by A1, A3;

      hence thesis by A2, ZFMISC_1: 74;

    end;

    definition

      let X be non empty TopSpace, x be Point of X;

      :: CONNSP_2:def3

      pred X is_locally_connected_in x means for U1 be Subset of X st U1 is a_neighborhood of x holds ex V be Subset of X st V is a_neighborhood of x & V is connected & V c= U1;

    end

    definition

      let X be non empty TopSpace;

      :: CONNSP_2:def4

      attr X is locally_connected means for x be Point of X holds X is_locally_connected_in x;

    end

    definition

      let X be non empty TopSpace, A be Subset of X, x be Point of X;

      :: CONNSP_2:def5

      pred A is_locally_connected_in x means for B be non empty Subset of X st A = B holds ex x1 be Point of (X | B) st x1 = x & (X | B) is_locally_connected_in x1;

    end

    definition

      let X be non empty TopSpace, A be non empty Subset of X;

      :: CONNSP_2:def6

      attr A is locally_connected means (X | A) is locally_connected;

    end

    theorem :: CONNSP_2:13



     Th13: for x holds X is_locally_connected_in x iff for V,S be Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds S is a_neighborhood of x

    proof

      let x;

      thus X is_locally_connected_in x implies for V,S be Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds S is a_neighborhood of x

      proof

        assume

         A1: X is_locally_connected_in x;

        let V,S be Subset of X such that

         A2: V is a_neighborhood of x and

         A3: S is_a_component_of V and

         A4: x in S;

        reconsider V9 = V as non empty Subset of X by A2, Th4;

        consider S1 be Subset of (X | V) such that

         A5: S1 = S and

         A6: S1 is a_component by A3, CONNSP_1:def 6;

        consider V1 be Subset of X such that

         A7: V1 is a_neighborhood of x and

         A8: V1 is connected and

         A9: V1 c= V by A1, A2;

        V1 c= ( [#] (X | V)) by A9, PRE_TOPC:def 5;

        then

        reconsider V2 = V1 as Subset of (X | V);



         A10: x in ( Int V1) by A7, Def1;

        V2 is connected by A8, CONNSP_1: 23;

        then V2 misses S1 or V2 c= S1 by A6, CONNSP_1: 36;

        then

         A11: (V2 /\ S1) = ( {} (X | V9)) or V2 c= S1 by XBOOLE_0:def 7;

        x in V2 by A7, Th4;

        then ( Int V1) c= ( Int S) by A4, A5, A11, TOPS_1: 19, XBOOLE_0:def 4;

        hence thesis by A10, Def1;

      end;

      assume

       A12: for V,S be Subset of X st V is a_neighborhood of x & S is_a_component_of V & x in S holds S is a_neighborhood of x;

      for U1 be Subset of X st U1 is a_neighborhood of x holds ex V be Subset of X st V is a_neighborhood of x & V is connected & V c= U1

      proof

        let U1 be Subset of X;



         A13: ( [#] (X | U1)) = U1 by PRE_TOPC:def 5;

        assume

         A14: U1 is a_neighborhood of x;

        then

         A15: x in U1 by Th4;

        reconsider U1 as non empty Subset of X by A14, Th4;

        x in ( [#] (X | U1)) by A15, PRE_TOPC:def 5;

        then

        reconsider x1 = x as Point of (X | U1);

        set S1 = ( Component_of x1);

        reconsider S = S1 as Subset of X by PRE_TOPC: 11;

        take S;

        S1 is a_component by CONNSP_1: 40;

        then

         A16: S is_a_component_of U1 by CONNSP_1:def 6;

        x in S & S1 is connected by CONNSP_1: 38;

        hence thesis by A12, A14, A13, A16, CONNSP_1: 23;

      end;

      hence thesis;

    end;

    theorem :: CONNSP_2:14



     Th14: for x holds X is_locally_connected_in x iff for U1 be non empty Subset of X st U1 is open & x in U1 holds ex x1 be Point of (X | U1) st x1 = x & x in ( Int ( Component_of x1))

    proof

      let x;



       A1: X is_locally_connected_in x implies for U1 be non empty Subset of X st U1 is open & x in U1 holds ex x1 be Point of (X | U1) st x1 = x & x in ( Int ( Component_of x1))

      proof

        assume

         A2: X is_locally_connected_in x;

        let U1 be non empty Subset of X such that

         A3: U1 is open and

         A4: x in U1;

        x in ( [#] (X | U1)) by A4, PRE_TOPC:def 5;

        then

        reconsider x1 = x as Point of (X | U1);

        reconsider S1 = ( Component_of x1) as Subset of (X | U1);

        take x1;

        reconsider S = S1 as Subset of X by PRE_TOPC: 11;



         A5: x in S by CONNSP_1: 38;

        S1 is a_component by CONNSP_1: 40;

        then

         A6: S is_a_component_of U1 by CONNSP_1:def 6;

        U1 is a_neighborhood of x by A3, A4, Th3;

        then S is a_neighborhood of x by A2, A6, A5, Th13;

        then S1 is a_neighborhood of x1 by Th10;

        hence thesis by Def1;

      end;

      (for U1 be non empty Subset of X st U1 is open & x in U1 holds ex x1 be Point of (X | U1) st x1 = x & x in ( Int ( Component_of x1))) implies X is_locally_connected_in x

      proof

        assume

         A7: for U1 be non empty Subset of X st U1 is open & x in U1 holds ex x1 be Point of (X | U1) st x1 = x & x in ( Int ( Component_of x1));

        for U1 be Subset of X st U1 is a_neighborhood of x holds ex V1 be Subset of X st V1 is a_neighborhood of x & V1 is connected & V1 c= U1

        proof

          let U1 be Subset of X;

          assume U1 is a_neighborhood of x;

          then

          consider V be non empty Subset of X such that

           A8: V is a_neighborhood of x and

           A9: V is open and

           A10: V c= U1 by Th5;

          consider x1 be Point of (X | V) such that

           A11: x1 = x and

           A12: x in ( Int ( Component_of x1)) by A7, A8, A9, Th4;

          set S1 = ( Component_of x1);

          reconsider S = S1 as Subset of X by PRE_TOPC: 11;

          take S;

          S1 c= ( [#] (X | V));

          then

           A13: S1 is connected & S c= V by PRE_TOPC:def 5;

          S1 is a_neighborhood of x1 by A11, A12, Def1;

          hence thesis by A9, A10, A11, A13, Th9, CONNSP_1: 23;

        end;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: CONNSP_2:15



     Th15: X is locally_connected implies for S be Subset of X st S is a_component holds S is open

    proof

      assume

       A1: X is locally_connected;

      let S be Subset of X such that

       A2: S is a_component;

      now

        let p be object;

        assume

         A3: p in S;

        then

        reconsider x = p as Point of X;



         A4: ( [#] X) is a_neighborhood of x by Th3;

        X is_locally_connected_in x & S is_a_component_of ( [#] X) by A1, A2, Th11;

        then S is a_neighborhood of x by A3, A4, Th13;

        hence p in ( Int S) by Def1;

      end;

      then ( Int S) c= S & S c= ( Int S) by TOPS_1: 16;

      then ( Int S) = S by XBOOLE_0:def 10;

      hence thesis;

    end;

    theorem :: CONNSP_2:16



     Th16: X is_locally_connected_in x implies for A be non empty Subset of X st A is open & x in A holds A is_locally_connected_in x

    proof

      assume

       A1: X is_locally_connected_in x;

      let A be non empty Subset of X such that

       A2: A is open and

       A3: x in A;

      reconsider B = A as non empty Subset of X;



       A4: ( [#] (X | A)) = A by PRE_TOPC:def 5;

      for C be non empty Subset of X st B = C holds ex x1 be Point of (X | C) st x1 = x & (X | C) is_locally_connected_in x1

      proof

        let C be non empty Subset of X;

        assume

         A5: B = C;

        then

        reconsider y = x as Point of (X | C) by A3, A4;

        take x1 = y;

        for U1 be Subset of (X | B) st U1 is a_neighborhood of x1 holds ex V be Subset of (X | B) st V is a_neighborhood of x1 & V is connected & V c= U1

        proof

          let U1 be Subset of (X | B) such that

           A6: U1 is a_neighborhood of x1;

          reconsider U2 = U1 as Subset of X by PRE_TOPC: 11;

          U2 is a_neighborhood of x by A2, A5, A6, Th9;

          then

          consider V be Subset of X such that

           A7: V is a_neighborhood of x & V is connected and

           A8: V c= U2 by A1;

          reconsider V1 = V as Subset of (X | B) by A8, XBOOLE_1: 1;

          take V1;

          thus thesis by A5, A7, A8, Th10, CONNSP_1: 23;

        end;

        hence thesis by A5;

      end;

      hence thesis;

    end;

    theorem :: CONNSP_2:17



     Th17: X is locally_connected implies for A be non empty Subset of X st A is open holds A is locally_connected

    proof

      assume

       A1: X is locally_connected;

      let A be non empty Subset of X such that

       A2: A is open;

      for x be Point of (X | A) holds (X | A) is_locally_connected_in x

      proof

        let x be Point of (X | A);

        x in ( [#] (X | A));

        then

         A3: x in A by PRE_TOPC:def 5;

        then

        reconsider x1 = x as Point of X;

        X is_locally_connected_in x1 by A1;

        then A is_locally_connected_in x1 by A2, A3, Th16;

        then ex x2 be Point of (X | A) st x2 = x1 & (X | A) is_locally_connected_in x2;

        hence thesis;

      end;

      then (X | A) is locally_connected;

      hence thesis;

    end;

    theorem :: CONNSP_2:18



     Th18: X is locally_connected iff for A be non empty Subset of X, B be Subset of X st A is open & B is_a_component_of A holds B is open

    proof

      thus X is locally_connected implies for A be non empty Subset of X, B be Subset of X st A is open & B is_a_component_of A holds B is open

      proof

        assume

         A1: X is locally_connected;

        let A be non empty Subset of X, B be Subset of X such that

         A2: A is open and

         A3: B is_a_component_of A;

        consider B1 be Subset of (X | A) such that

         A4: B1 = B and

         A5: B1 is a_component by A3, CONNSP_1:def 6;

        reconsider B1 as Subset of (X | A);

        A is locally_connected by A1, A2, Th17;

        then (X | A) is locally_connected;

        then B1 is open by A5, Th15;

        then B1 in the topology of (X | A) by PRE_TOPC:def 2;

        then

        consider B2 be Subset of X such that

         A6: B2 in the topology of X and

         A7: B1 = (B2 /\ ( [#] (X | A))) by PRE_TOPC:def 4;



         A8: B = (B2 /\ A) by A4, A7, PRE_TOPC:def 5;

        reconsider B2 as Subset of X;

        B2 is open by A6, PRE_TOPC:def 2;

        hence thesis by A2, A8;

      end;

      assume

       A9: for A be non empty Subset of X, B be Subset of X st A is open & B is_a_component_of A holds B is open;

      let x;

      for U1 be non empty Subset of X st U1 is open & x in U1 holds ex x1 be Point of (X | U1) st x1 = x & x in ( Int ( Component_of x1))

      proof

        let U1 be non empty Subset of X such that

         A10: U1 is open and

         A11: x in U1;

        x in ( [#] (X | U1)) by A11, PRE_TOPC:def 5;

        then

        reconsider x1 = x as Point of (X | U1);

        set S1 = ( Component_of x1);

        reconsider S = S1 as Subset of X by PRE_TOPC: 11;

        S1 is a_component by CONNSP_1: 40;

        then S is_a_component_of U1 by CONNSP_1:def 6;

        then

         A12: S is open by A9, A10;

        take x1;

        x in S by CONNSP_1: 38;

        then S1 is a_neighborhood of x1 by A12, Th3, Th10;

        hence thesis by Def1;

      end;

      hence thesis by Th14;

    end;

    theorem :: CONNSP_2:19

    X is locally_connected implies for E be non empty Subset of X, C be non empty Subset of (X | E) st C is connected & C is open holds ex H be Subset of X st H is open & H is connected & C = (E /\ H)

    proof

      assume

       A1: X is locally_connected;

      let E be non empty Subset of X, C be non empty Subset of (X | E) such that

       A2: C is connected and

       A3: C is open;

      C in the topology of (X | E) by A3, PRE_TOPC:def 2;

      then

      consider G be Subset of X such that

       A4: G in the topology of X and

       A5: C = (G /\ ( [#] (X | E))) by PRE_TOPC:def 4;



       A6: C = (G /\ E) by A5, PRE_TOPC:def 5;

      reconsider G as non empty Subset of X by A5;



       A7: G is open by A4, PRE_TOPC:def 2;

      reconsider C1 = C as Subset of X by PRE_TOPC: 11;

      C <> ( {} (X | E));

      then

      consider x be Point of (X | E) such that

       A8: x in C by PRE_TOPC: 12;

      x in G by A5, A8, XBOOLE_0:def 4;

      then x in ( [#] (X | G)) by PRE_TOPC:def 5;

      then

      reconsider y = x as Point of (X | G);

      set H1 = ( Component_of y);

      reconsider H = H1 as Subset of X by PRE_TOPC: 11;

      take H;



       A9: H1 is a_component by CONNSP_1: 40;

      then H is_a_component_of G by CONNSP_1:def 6;

      hence H is open by A1, A7, Th18;

      C c= G by A5, XBOOLE_1: 17;

      then C c= ( [#] (X | G)) by PRE_TOPC:def 5;

      then

      reconsider C2 = C1 as Subset of (X | G);

      H1 c= ( [#] (X | G));

      then

       A10: H c= G by PRE_TOPC:def 5;

      C1 is connected by A2, CONNSP_1: 23;

      then C2 is connected by CONNSP_1: 23;

      then C2 misses H or C2 c= H by A9, CONNSP_1: 36;

      then

       A11: (C2 /\ H) = ( {} (X | G)) or C2 c= H by XBOOLE_0:def 7;



       A12: x in H1 by CONNSP_1: 38;

      (H /\ (G /\ E)) c= C by A6, XBOOLE_0:def 4;

      then ((H /\ G) /\ E) c= C by XBOOLE_1: 16;

      then

       A13: (E /\ H) c= C by A10, XBOOLE_1: 28;

      thus H is connected by CONNSP_1: 23;

      C c= E by A6, XBOOLE_1: 17;

      then C c= (E /\ H) by A8, A11, A12, XBOOLE_0:def 4;

      hence thesis by A13, XBOOLE_0:def 10;

    end;

    theorem :: CONNSP_2:20



     Th20: X is normal iff for A,C be Subset of X st A <> {} & C <> ( [#] X) & A c= C & A is closed & C is open holds ex G be Subset of X st G is open & A c= G & ( Cl G) c= C

    proof

      thus X is normal implies for A,C be Subset of X st A <> {} & C <> ( [#] X) & A c= C & A is closed & C is open holds ex G be Subset of X st G is open & A c= G & ( Cl G) c= C

      proof

        assume

         A1: for A,B be Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B holds ex G,H be Subset of X st G is open & H is open & A c= G & B c= H & G misses H;

        let A,C be Subset of X such that

         A2: A <> {} and

         A3: C <> ( [#] X) and

         A4: A c= C and

         A5: A is closed and

         A6: C is open;

        set B = (( [#] X) \ C);

        B c= (A ` ) by A4, XBOOLE_1: 34;

        then

         A7: A misses B by SUBSET_1: 23;

        B <> {} & (C ` ) is closed by A3, A6, PRE_TOPC: 4;

        then

        consider G,H be Subset of X such that

         A8: G is open and

         A9: H is open and

         A10: A c= G and

         A11: B c= H and

         A12: G misses H by A1, A2, A5, A7;

        take G;

        for p be object holds p in ( Cl G) implies p in C

        proof

          let p be object;

          assume

           A13: p in ( Cl G);

          then

          reconsider y = p as Point of X;

          (H ` ) is closed & G c= (H ` ) by A9, A12, SUBSET_1: 23;

          then

           A14: y in (H ` ) by A13, PRE_TOPC: 15;

          (H ` ) c= (B ` ) by A11, SUBSET_1: 12;

          then y in (B ` ) by A14;

          hence thesis by PRE_TOPC: 3;

        end;

        hence thesis by A8, A10;

      end;

      assume

       A15: for A,C be Subset of X st A <> {} & C <> ( [#] X) & A c= C & A is closed & C is open holds ex G be Subset of X st G is open & A c= G & ( Cl G) c= C;

      for A,B be Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B holds ex G,H be Subset of X st G is open & H is open & A c= G & B c= H & G misses H

      proof

        let A,B be Subset of X such that

         A16: A <> {} and

         A17: B <> {} and

         A18: A is closed and

         A19: B is closed & A misses B;

        set C = (( [#] X) \ B);

        (( [#] X) \ C) = B by PRE_TOPC: 3;

        then

         A20: C <> ( [#] X) by A17, PRE_TOPC: 4;

        A c= (B ` ) & C is open by A19, PRE_TOPC:def 3, SUBSET_1: 23;

        then

        consider G be Subset of X such that

         A21: G is open and

         A22: A c= G and

         A23: ( Cl G) c= C by A15, A16, A18, A20;

        take G;

        take H = (( [#] X) \ ( Cl G));

        thus G is open & H is open by A21, PRE_TOPC:def 3;

        (C ` ) c= (( Cl G) ` ) by A23, SUBSET_1: 12;

        hence A c= G & B c= H by A22, PRE_TOPC: 3;

        H c= (G ` ) by PRE_TOPC: 18, XBOOLE_1: 34;

        hence thesis by SUBSET_1: 23;

      end;

      hence thesis;

    end;

    theorem :: CONNSP_2:21

    X is locally_connected & X is normal implies for A,B be Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B holds (A is connected & B is connected implies ex R,S be Subset of X st R is connected & S is connected & R is open & S is open & A c= R & B c= S & R misses S)

    proof

      assume that

       A1: X is locally_connected and

       A2: X is normal;

      let A,B be Subset of X such that

       A3: A <> {} and

       A4: B <> {} and

       A5: A is closed and

       A6: B is closed & A misses B;

      B = (( [#] X) \ (( [#] X) \ B)) by PRE_TOPC: 3;

      then

       A7: (( [#] X) \ B) <> ( [#] X) by A4, PRE_TOPC: 4;

      A <> ( {} X) by A3;

      then

      consider x be Point of X such that

       A8: x in A by PRE_TOPC: 12;

      A c= (B ` ) & (B ` ) is open by A6, SUBSET_1: 23;

      then

      consider G be Subset of X such that

       A9: G is open and

       A10: A c= G and

       A11: ( Cl G) c= (B ` ) by A2, A3, A5, A7, Th20;



       A12: ( Cl G) misses B by A11, SUBSET_1: 23;



       A13: x in G by A10, A8;

      reconsider G as non empty Subset of X by A3, A10;

      x in ( [#] (X | G)) by A13, PRE_TOPC:def 5;

      then

      reconsider y = x as Point of (X | G);



       A14: ( Cl G) misses (( Cl G) ` ) by XBOOLE_1: 79;

      assume that

       A15: A is connected and

       A16: B is connected;

      set H = ( Component_of y);

      reconsider H1 = H as Subset of X by PRE_TOPC: 11;

      take R = H1;



       A17: H is a_component by CONNSP_1: 40;

      then

       A18: H1 is_a_component_of G by CONNSP_1:def 6;

      A c= ( [#] (X | G)) by A10, PRE_TOPC:def 5;

      then

      reconsider A1 = A as Subset of (X | G);



       A19: H is connected & y in H by CONNSP_1: 38;

      A1 is connected by A15, CONNSP_1: 23;

      then A1 misses H or A1 c= H by A17, CONNSP_1: 36;

      then

       A20: (A1 /\ H) = {} or A1 c= H by XBOOLE_0:def 7;

      H c= ( [#] (X | G));

      then

       A21: R c= G by PRE_TOPC:def 5;

      G c= ( Cl G) by PRE_TOPC: 18;

      then

       A22: R c= ( Cl G) by A21;

      B <> ( {} X) by A4;

      then

      consider z be Point of X such that

       A23: z in B by PRE_TOPC: 12;



       A24: B c= (( Cl G) ` ) by A12, SUBSET_1: 23;

      then

      reconsider C = (( Cl G) ` ) as non empty Subset of X by A23;

      z in (( Cl G) ` ) by A23, A24;

      then z in ( [#] (X | C)) by PRE_TOPC:def 5;

      then

      reconsider z1 = z as Point of (X | C);

      set V = ( Component_of z1);

      reconsider V1 = V as Subset of X by PRE_TOPC: 11;

      take S = V1;



       A25: V is a_component by CONNSP_1: 40;

      B c= ( [#] (X | (( Cl G) ` ))) by A24, PRE_TOPC:def 5;

      then

      reconsider B1 = B as Subset of (X | (( Cl G) ` ));



       A26: V is connected & z1 in V by CONNSP_1: 38;

      B1 is connected by A16, CONNSP_1: 23;

      then B1 misses V or B1 c= V by A25, CONNSP_1: 36;

      then

       A27: (B1 /\ V) = {} or B1 c= V by XBOOLE_0:def 7;

      V c= ( [#] (X | (( Cl G) ` )));

      then S c= (( Cl G) ` ) by PRE_TOPC:def 5;

      then (R /\ S) c= (( Cl G) /\ (( Cl G) ` )) by A22, XBOOLE_1: 27;

      then (R /\ S) c= ( {} X) by A14, XBOOLE_0:def 7;

      then

       A28: (R /\ S) = {} ;

      V1 is_a_component_of (( Cl G) ` ) by A25, CONNSP_1:def 6;

      hence thesis by A1, A9, A8, A18, A20, A19, A23, A27, A26, A28, Th18, CONNSP_1: 23, XBOOLE_0:def 4, XBOOLE_0:def 7;

    end;

    theorem :: CONNSP_2:22



     Th22: for x be Point of X, F be Subset-Family of X st for A be Subset of X holds A in F iff A is open closed & x in A holds F <> {}

    proof



       A1: ( [#] X) is open closed;

      let x be Point of X, F be Subset-Family of X;

      assume for A be Subset of X holds A in F iff A is open closed & x in A;

      hence thesis by A1;

    end;

    definition

      let X be non empty TopSpace, x be Point of X;

      :: CONNSP_2:def7

      func qComponent_of x -> Subset of X means

      : Def7: ex F be Subset-Family of X st (for A be Subset of X holds A in F iff A is open closed & x in A) & ( meet F) = it ;

      existence

      proof

        defpred P[ set] means ex A1 be Subset of X st A1 = $1 & A1 is open closed & x in $1;

        consider F be Subset-Family of X such that

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

        reconsider S = ( meet F) as Subset of X;

        take S, F;

        thus for A be Subset of X holds A in F iff A is open closed & x in A

        proof

          let A be Subset of X;

          thus A in F implies A is open closed & x in A

          proof

            assume A in F;

            then ex A1 be Subset of X st A1 = A & A1 is open closed & x in A by A1;

            hence thesis;

          end;

          thus thesis by A1;

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let S,S9 be Subset of X;

        assume that

         A2: ex F be Subset-Family of X st (for A be Subset of X holds A in F iff A is open closed & x in A) & ( meet F) = S and

         A3: ex F9 be Subset-Family of X st (for A be Subset of X holds A in F9 iff A is open closed & x in A) & ( meet F9) = S9;

        consider F be Subset-Family of X such that

         A4: for A be Subset of X holds A in F iff A is open closed & x in A and

         A5: ( meet F) = S by A2;

        consider F9 be Subset-Family of X such that

         A6: for A be Subset of X holds A in F9 iff A is open closed & x in A and

         A7: ( meet F9) = S9 by A3;



         A8: F9 <> {} by A6, Th22;



         A9: F <> {} by A4, Th22;

        now

          let y be object;

           A10:

          now

            assume

             A11: y in S9;

            for B be set st B in F holds y in B

            proof

              let B be set;

              assume

               A12: B in F;

              then

              reconsider B1 = B as Subset of X;

              B1 is open closed & x in B1 by A4, A12;

              then B1 in F9 by A6;

              hence thesis by A7, A11, SETFAM_1:def 1;

            end;

            hence y in S by A5, A9, SETFAM_1:def 1;

          end;

          now

            assume

             A13: y in S;

            for B be set st B in F9 holds y in B

            proof

              let B be set;

              assume

               A14: B in F9;

              then

              reconsider B1 = B as Subset of X;

              B1 is open closed & x in B1 by A6, A14;

              then B1 in F by A4;

              hence thesis by A5, A13, SETFAM_1:def 1;

            end;

            hence y in S9 by A7, A8, SETFAM_1:def 1;

          end;

          hence y in S iff y in S9 by A10;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: CONNSP_2:23

    x in ( qComponent_of x)

    proof

      consider F be Subset-Family of X such that

       A1: for A be Subset of X holds A in F iff A is open closed & x in A and

       A2: ( qComponent_of x) = ( meet F) by Def7;

      F <> {} & for A be set holds A in F implies x in A by A1, Th22;

      hence thesis by A2, SETFAM_1:def 1;

    end;

    theorem :: CONNSP_2:24

    for A be Subset of X st A is open closed & x in A holds A c= ( qComponent_of x) implies A = ( qComponent_of x)

    proof

      let A be Subset of X;

      consider F be Subset-Family of X such that

       A1: for A be Subset of X holds (A in F iff A is open closed & x in A) and

       A2: ( qComponent_of x) = ( meet F) by Def7;

      assume A is open closed & x in A;

      then A in F by A1;

      then

       A3: ( qComponent_of x) c= A by A2, SETFAM_1: 3;

      assume A c= ( qComponent_of x);

      hence thesis by A3, XBOOLE_0:def 10;

    end;

    theorem :: CONNSP_2:25

    ( qComponent_of x) is closed

    proof

      consider F be Subset-Family of X such that

       A1: for A be Subset of X holds (A in F iff A is open closed & x in A) and

       A2: ( qComponent_of x) = ( meet F) by Def7;

      for A be Subset of X st A in F holds A is closed by A1;

      hence thesis by A2, PRE_TOPC: 14;

    end;

    theorem :: CONNSP_2:26

    ( Component_of x) c= ( qComponent_of x)

    proof

      consider F9 be Subset-Family of X such that

       A1: for A be Subset of X holds (A in F9 iff A is open closed & x in A) and

       A2: ( qComponent_of x) = ( meet F9) by Def7;



       A3: for B1 be set st B1 in F9 holds ( Component_of x) c= B1

      proof

        set S = ( Component_of x);

        let B1 be set;



         A4: x in S by CONNSP_1: 38;

        assume

         A5: B1 in F9;

        then

        reconsider B = B1 as Subset of X;



         A6: x in B by A1, A5;



         A7: B is open closed by A1, A5;

        then (B ` ) is closed;

        then ( Cl (B ` )) = (B ` ) by PRE_TOPC: 22;

        then

         A8: B misses ( Cl (B ` )) by XBOOLE_1: 79;



         A9: (S /\ B) c= B & (S /\ (B ` )) c= (B ` ) by XBOOLE_1: 17;

        ( Cl B) = B by A7, PRE_TOPC: 22;

        then ( Cl B) misses (B ` ) by XBOOLE_1: 79;

        then (B,(B ` )) are_separated by A8, CONNSP_1:def 1;

        then

         A10: ((S /\ B),(S /\ (B ` ))) are_separated by A9, CONNSP_1: 7;



         A11: ( [#] X) = (B \/ (B ` )) by PRE_TOPC: 2;

        S = (S /\ ( [#] X)) by XBOOLE_1: 28

        .= ((S /\ B) \/ (S /\ (B ` ))) by A11, XBOOLE_1: 23;

        then (S /\ B) = ( {} X) or (S /\ (B ` )) = ( {} X) by A10, CONNSP_1: 15;

        then S misses (B ` ) by A6, A4, XBOOLE_0:def 4, XBOOLE_0:def 7;

        then S c= ((B ` ) ` ) by SUBSET_1: 23;

        hence thesis;

      end;

      F9 <> {} by A1, Th22;

      hence thesis by A2, A3, SETFAM_1: 5;

    end;

    theorem :: CONNSP_2:27

    for T be non empty TopSpace, A be Subset of T holds for p be Point of T holds p in ( Cl A) iff for G be a_neighborhood of p holds G meets A

    proof

      let T be non empty TopSpace, A be Subset of T;

      let p be Point of T;

      hereby

        assume

         A1: p in ( Cl A);

        let G be a_neighborhood of p;

        p in ( Int G) & ( Int G) is open by Def1;

        then A meets ( Int G) by A1, PRE_TOPC:def 7;

        hence G meets A by TOPS_1: 16, XBOOLE_1: 63;

      end;

      assume

       A2: for G be a_neighborhood of p holds G meets A;

      now

        let G be Subset of T;

        assume G is open & p in G;

        then G is a_neighborhood of p by Th3;

        hence A meets G by A2;

      end;

      hence thesis by PRE_TOPC:def 7;

    end;

    theorem :: CONNSP_2:28

    for X be non empty TopSpace, A be Subset of X holds ( [#] X) is a_neighborhood of A

    proof

      let X be non empty TopSpace, A be Subset of X;

      ( Int ( [#] X)) = ( [#] X) by TOPS_1: 15;

      hence A c= ( Int ( [#] X));

    end;

    theorem :: CONNSP_2:29

    for X be non empty TopSpace, A be Subset of X, Y be a_neighborhood of A holds A c= Y

    proof

      let X be non empty TopSpace, A be Subset of X, Y be a_neighborhood of A;

      A c= ( Int Y) & ( Int Y) c= Y by Def2, TOPS_1: 16;

      hence thesis;

    end;