CONNSP_2

:: Locally Connected Spaces
::  by Beata Padlewska
::
:: Received September 5, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, PRE_TOPC, SUBSET_1, TOPS_1, TARSKI, RCOMP_1, RELAT_1,
      CONNSP_1, RELAT_2, SETFAM_1, CONNSP_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, DOMAIN_1, STRUCT_0, PRE_TOPC,
      TOPS_1, CONNSP_1;
 constructors SETFAM_1, DOMAIN_1, TOPS_1, CONNSP_1, COMPTS_1;
 registrations XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, COMPTS_1;
 equalities SUBSET_1, STRUCT_0;
 expansions TARSKI, COMPTS_1;
 theorems TARSKI, ZFMISC_1, SETFAM_1, PRE_TOPC, TOPS_1, CONNSP_1, XBOOLE_0,
      XBOOLE_1, SUBSET_1;
 schemes SUBSET_1;

begin

::
::            A NEIGHBORHOOD OF A POINT
::

definition
  let X be non empty TopSpace, x be Point of X;
  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;

::
::               A NEIGHBORHOOD OF A SET
::

definition
  let X be TopSpace,A be Subset of X;
  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
  for A,B being 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
  for A,B being 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 Th3:
  for U1 being Subset of X, x being 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 Th4:
  for U1 being Subset of X, x being 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 Th5:
  U1 is a_neighborhood of x implies ex V being 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 being 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 Th6:
  U1 is a_neighborhood of x iff ex V being 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 being 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 being Subset of X st V is open & V c= U1 & x in V by A2,Th4;
  end;
  now
    given V being 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
  for U1 being Subset of X holds U1 is open iff for x st x in U1 ex A
  being 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 ex A being Subset of X st A is a_neighborhood of
    x & A c= U1;
    for x being set holds x in U1 iff ex V being 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 being 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 being Subset of X such that
A3:     S is a_neighborhood of x and
A4:     S c= U1 by A1,A2;
        consider V being 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 being 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
  for V being 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 being 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 Th9:
  for B being non empty Subset of X, x being Point of X|B, A being
  Subset of X|B, A1 being Subset of X, x1 being 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 being 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 being 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 being SubSpace of X, A being Subset of X, A1 being 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 being Subset of X such that
A3: Q is open and
A4: Q c= A & p in Q by TOPS_1:22;
    ex Q1 being 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 Th10:
  for B being non empty Subset of X, x being Point of X|B, A being
  Subset of X|B, A1 being Subset of X, x1 being 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 Th11:
  for A being Subset of X, B being 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 being 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 being 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
  for X1 being non empty SubSpace of X, x being Point of X, x1 being
  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 being Subset-Family of X such that
A1: for A being 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,38;
  assume x = x1;
  then Z in F by A1,A3;
  hence thesis by A2,ZFMISC_1:74;
end;

::
::            LOCALLY CONNECTED TOPOLOGICAL SPACES
::

definition
  let X be non empty TopSpace, x be Point of X;
  pred X is_locally_connected_in x means

  for U1 being Subset of X st U1
  is a_neighborhood of x ex V being Subset of X st V is a_neighborhood of x & V
  is connected & V c= U1;
end;

definition
  let X be non empty TopSpace;
  attr X is locally_connected means

  for x being 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;
  pred A is_locally_connected_in x means

  for B being non empty Subset
of X st A = B ex x1 being 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;
  attr A is locally_connected means

  X|A is locally_connected;
end;

theorem Th13:
  for x holds X is_locally_connected_in x iff for V,S being 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 being 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 being Subset of X|V such that
A5: S1=S and
A6: S1 is a_component by A3,CONNSP_1:def 6;
    consider V1 being 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 being 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 being Subset of X st U1 is a_neighborhood of x ex V being 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 Th14:
  for x holds X is_locally_connected_in x iff for U1 being non
empty Subset of X st U1 is open & x in U1 ex x1 being 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 being non empty Subset of X
  st U1 is open & x in U1 ex x1 being 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 being non empty Subset of X st U1 is open & x in U1 ex x1 being
  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 being non empty Subset of X st U1 is open & x in U1 ex x1
    being Point of X|U1 st x1=x & x in Int(Component_of x1);
    for U1 being Subset of X st U1 is a_neighborhood of x ex V1 being
    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 being 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 being 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 Th15:
  X is locally_connected implies
  for S being 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 Th16:
  X is_locally_connected_in x implies for A being 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 being non empty Subset of X st B = C ex x1 being 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 being Subset of X|B st U1 is a_neighborhood of x1 ex V being
    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 being 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 Th17:
  X is locally_connected implies for A being 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 being 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 being 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 Th18:
  X is locally_connected iff for A being non empty Subset of X, B
  being 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 being non empty Subset of X, B
  being 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 being 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 being 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 being non empty Subset of X, B being Subset of X st A is open
  & B is_a_component_of A holds B is open;
  let x;
  for U1 being non empty Subset of X st U1 is open & x in U1 ex x1 being
  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
  X is locally_connected implies for E being non empty Subset of X, C
  being non empty Subset of X|E st C is connected & C is open ex H being 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 being 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 being 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 Th20:
  X is normal iff for A,C being Subset of X st A <> {} & C <> [#]
X & A c= C & A is closed & C is open ex G being Subset of X st G is open & A c=
  G & Cl G c= C
proof
  thus X is normal implies for A,C being Subset of X st A <> {} & C <> [#] X &
A c= C & A is closed & C is open ex G being Subset of X st G is open & A c= G &
  Cl G c= C
  proof
    assume
A1: for A,B being Subset of X st A <> {} & B <> {} & A is closed & B
is closed & A misses B ex G,H being 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 being 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 being 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 being Subset of X st A <> {} & C <> [#] X & A c= C & A is
  closed & C is open ex G being Subset of X st G is open & A c= G & Cl G c= C;
  for A,B being Subset of X st A <> {} & B <> {} & A is closed & B is
closed & A misses B ex G,H being 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 being 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
  X is locally_connected & X is normal implies for A,B being 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 being 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 being 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 being 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 being 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,def 7;
end;

theorem Th22:
  for x being Point of X, F being Subset-Family of X st for A
  being 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 being Subset of X holds A in F iff A is open closed & x in A;
  hence thesis by A1;
end;

::
::             A QUASICOMPONENT OF A POINT
::

definition
  let X be non empty TopSpace, x be Point of X;
  func qComponent_of x -> Subset of X means
  :Def7:
  ex F being Subset-Family of
  X st (for A being 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 being Subset of X st A1 = $1 & A1 is open
    closed & x in $1;
    consider F being Subset-Family of X such that
A1: for A being 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 being 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 being 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 being Subset-Family of X st (for A being Subset of X holds A
    in F iff A is open closed & x in A) & meet F = S and
A3: ex F9 being Subset-Family of X st (for A being Subset of X holds
    A in F9 iff A is open closed & x in A) & meet F9 = S9;
    consider F being Subset-Family of X such that
A4: for A being Subset of X holds A in F iff A is open closed & x in A and
A5: meet F = S by A2;
    consider F9 being Subset-Family of X such that
A6: for A being 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 being 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 being 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
  x in qComponent_of x
proof
  consider F being Subset-Family of X such that
A1: for A being 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 being set holds A in F implies x in A by A1,Th22;
  hence thesis by A2,SETFAM_1:def 1;
end;

theorem
  for A being 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 being Subset-Family of X such that
A1: for A being 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
  qComponent_of x is closed
proof
  consider F being Subset-Family of X such that
A1: for A being 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 being Subset of X st A in F holds A is closed by A1;
  hence thesis by A2,PRE_TOPC:14;
end;

theorem
  Component_of x c= qComponent_of x
proof
  consider F9 being Subset-Family of X such that
A1: for A being 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 being 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,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;

:: Moved from YELLOW_6, AG 18.02.2006

theorem
  for T being non empty TopSpace, A being Subset of T for p being Point
  of T holds p in Cl A iff for G being 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 being 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
  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
  for X be non empty TopSpace, A be Subset of X, Y being 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;