:: Components and Unions of Components
::  by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received February 5, 1996
:: Copyright (c) 1996-2012 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, CONNSP_1, SETFAM_1, RELAT_2,
      TARSKI, STRUCT_0, ZFMISC_1, RELAT_1, RUSUB_4, RCOMP_1, CONNSP_3;
 notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, STRUCT_0, PRE_TOPC, CONNSP_1;
 constructors SETFAM_1, CONNSP_1;
 registrations SUBSET_1, STRUCT_0, PRE_TOPC, CONNSP_1;
 requirements SUBSET, BOOLE;
 definitions TARSKI, XBOOLE_0, STRUCT_0;
 theorems TARSKI, ZFMISC_1, SETFAM_1, PRE_TOPC, SUBSET_1, CONNSP_1, XBOOLE_0,
      XBOOLE_1, ORDERS_1;
 schemes SUBSET_1;

begin :: The component of a subset in a topological space

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;
  func Component_of V -> Subset of GX means
  :Def1:
  ex F being Subset-Family of GX st
  (for A being Subset of GX holds A in F iff A is connected & V c= A) &
  union F = it;
  existence
  proof
    defpred P[set] means ex A1 being Subset of GX st A1 = $1 & A1 is connected
    & V c= $1;
    consider F being Subset-Family of GX such that
A1: for A being Subset of GX holds A in F iff P[A] from SUBSET_1:sch 3;
    take union F, F;
    thus for A being 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 being 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 being Subset-Family of GX st (for A being Subset of GX holds
    A in F iff A is connected & V c= A) & union F = S and
A3: ex F9 being Subset-Family of GX st (for A being Subset of GX holds
    A in F9 iff A is connected & V c= A) & union F9 = S9;
    consider F being Subset-Family of GX such that
A4: for A being Subset of GX holds A in F iff A is connected & V c= A and
A5: union F = S by A2;
    consider F9 being Subset-Family of GX such that
A6: for A being Subset of GX holds A in F9 iff A is connected & V c= A and
A7: union F9 = S9 by A3;
    now
      let y be set;
A8:   now
        assume y in S9;
        then consider B being 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 being 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:1;
  end;
end;

theorem Th1:
  for GX being TopSpace, V being Subset of GX st (ex A being Subset
  of GX st A is connected & V c= A) holds V c= Component_of V
proof
  let GX be TopSpace, V be Subset of GX;
  given A being Subset of GX such that
A1: A is connected & V c= A;
  consider F being Subset-Family of GX such that
A2: for A being Subset of GX holds A in F iff A is connected & V c= A and
A3: Component_of V = union F by Def1;
A4: for A being set 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,XBOOLE_1:1;
end;

theorem
  for GX being TopSpace, V being Subset of GX st (not ex A being 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 being Subset of GX st A is connected & V c= A;
  consider F being Subset-Family of GX such that
A2: for A being Subset of GX holds A in F iff A is connected & V c= A and
A3: Component_of V = union F by Def1;
  now
    assume F <> {};
    then consider A being 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 Th3:
  Component_of {}GX = the carrier of GX
proof
  defpred P[set] means ex A1 being Subset of GX st A1 = $1 & A1 is connected &
  {}GX c= $1;
  consider F being Subset-Family of GX such that
A1: for A being Subset of GX holds A in F iff P[A] from SUBSET_1:sch 3;
A2: for A being Subset of GX holds A in F iff A is connected & {}GX c= A
  proof
    let A be Subset of GX;
    thus A in F implies A is connected & {}GX c= A
    proof
      assume A in F;
      then
      ex A1 being 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 set;
    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 by XBOOLE_1:2;
      hence Y in F by A2;
    end;
    given Y being 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
  for V being 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 Th5:
  for GX being TopSpace, V being 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 being Subset-Family of GX such that
A3: for A being Subset of GX holds A in F iff A is connected & V c= A and
A4: Component_of V = union F by Def1;
A5: for A being set st A in F holds V c= A by A3;
  F <> {} by A1,A3;
  then V c= meet F by A5,SETFAM_1:5;
  then
A6: meet F<>{}(GX) by A2;
  for A being Subset of GX st A in F holds A is connected by A3;
  hence thesis by A4,A6,CONNSP_1:26;
end;

theorem Th6:
  for V,C being 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 being Subset-Family of GX such that
A4: for A being Subset of GX holds (A in F iff A is connected & V c= A) and
A5: Component_of V = union F by Def1;
  V c= Component_of V by A1,Th1;
  then V c= C by A3,XBOOLE_1:1;
  then C in F by A2,A4;
  then C c= Component_of V by A5,ZFMISC_1:74;
  hence thesis by A3,XBOOLE_0:def 10;
end;

theorem Th7:
  for A being 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 Th8:
  for A being Subset of GX holds A is a_component iff ex V
  being Subset of GX st V is connected & V <> {} & A = Component_of V
proof
  let 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 being Subset of GX such that
A3: V is connected & V<>{} & A = Component_of V;
    A is connected & for B being 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
  for V being Subset of GX st V is connected & V<>{} holds Component_of
  V is a_component by Th8;

theorem
  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,34;
end;

theorem Th11:
  for V being 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 Th12:
  for A,B being Subset of GX st A is connected & B is connected &
  A<>{} & A c= B holds Component_of A = Component_of B
proof
  let 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,XBOOLE_1:1;
A8: Component_of B c= Component_of A
  proof
    consider F being Subset-Family of GX such that
A9: for D being Subset of GX holds D in F iff D is connected & A c= D and
A10: union F = Component_of A by Def1;
    Component_of B in F by A7,A5,A9;
    hence 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 being Subset-Family of GX such that
A12: for D being Subset of GX holds D in F iff D is connected & B c= D and
A13: union F = Component_of B by Def1;
    B c= Component_of A by A6,A8,XBOOLE_1:1;
    then Component_of A in F by A11,A12;
    hence thesis by A13,ZFMISC_1:74;
  end;
  hence thesis by A8,XBOOLE_0:def 10;
end;

theorem Th13:
  for A,B being Subset of GX st A is connected & B is connected &
  A<>{} & A c= B holds B c= Component_of A
proof
  let 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 Th14:
  for A being Subset of GX,B being 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 Th15:
  for A being Subset of GX, p being 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
  for A,B being Subset of GX st A is connected & B is connected & A
  meets B holds A \/ B c= Component_of A & A \/ B c= Component_of B & A c=
  Component_of B & B c= Component_of A
proof
  let A,B be Subset of GX;
A1: A c= A \/ B & B c= A \/ B by XBOOLE_1:7;
A2: for C,D being Subset of GX st C is connected & D is connected & C /\ D
  <>{} holds C \/ D c= Component_of C
  proof
    let C,D be Subset of GX;
    assume that
A3: C is connected and
A4: D is connected and
A5: C /\ D <>{};
    C meets D by A5,XBOOLE_0:def 7;
    then
A6: C \/ D is connected by A3,A4,CONNSP_1: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,XBOOLE_1:1;
end;

theorem
  for A being 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
  for A,B being Subset of GX st A is a_component & B is connected
  & B<>{} & A misses B holds A misses Component_of B
proof
  let 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 being Point of GX such that
A5: x in A /\ Component_of B by SUBSET_1:4;
  x in A by A5,XBOOLE_0:def 4;
  then
A6: Component_of x=Component_of A by A4,Th15;
A7: x in Component_of B by A5,XBOOLE_0:def 4;
  Component_of A=A & Component_of B=Component_of Component_of B by A1,A2,Th7
,Th11;
  then (Component_of B) /\ B={} by A2,A3,A7,A6,Th5,Th15;
  hence contradiction by A2,Th1,XBOOLE_1:28;
end;

begin :: On unions of components

Lm1: now
  let GX be TopStruct;
  reconsider S={} as Subset-Family of GX by XBOOLE_1:2;
  for B being Subset of GX st B in S holds B is a_component;
  hence ex F being Subset-Family of GX st (for B being Subset of GX st B in F
  holds B is a_component) & {}(GX)=union F by ZFMISC_1:2;
end;

definition
  let GX be TopStruct;
  mode a_union_of_components of GX -> Subset of GX means
    :Def2:
    ex F being
    Subset-Family of GX st (for B being Subset of GX st B in F holds B
    is a_component) & it = union F;
  existence
  proof
    take {}GX;
    thus thesis by Lm1;
  end;
end;

theorem Th19:
  {}(GX) is a_union_of_components of GX
proof
  thus ex F being Subset-Family of GX st (for B being Subset of GX st B in F
  holds B is a_component) & {}(GX) = union F by Lm1;
end;

theorem Th20:
  for A being 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;
    assume x in {B : B is a_component};
    then ex B being 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 being 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 being Subset of GX st B=B2 & B2 is a_component;
    hence thesis;
  end;
  the carrier of GX c= union S
  proof
    let x;
    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 by XBOOLE_0:def 10;
  assume A=(the carrier of GX);
  hence thesis by A2,A1,Def2;
end;

theorem Th21:
  for A being Subset of GX,p being Point of GX st p in A & A is
  a_union_of_components of GX holds Component_of p c= A
proof
  let 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 being Subset-Family of GX such that
A3: for B being Subset of GX st B in F holds B is a_component and
A4: A=union F by A2,Def2;
  consider X 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
  for A,B being Subset of GX st A is a_union_of_components of GX & B is
a_union_of_components of GX holds A \/ B is a_union_of_components of GX & A /\
  B is a_union_of_components of GX
proof
  let 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 being Subset-Family of GX such that
A3: for Ba being Subset of GX st Ba in Fa holds Ba is a_component and
A4: A=union Fa by A1,Def2;
  consider Fb being Subset-Family of GX such that
A5: for Bb being Subset of GX st Bb in Fb holds Bb is a_component and
A6: B=union Fb by A2,Def2;
A7: for B2 being Subset of GX st B2 in Fa \/ Fb holds B2 is a_component
  proof
    let B2 be Subset of GX;
    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 being 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 set;
      assume
A11:  x in A /\ B;
      then x in A by XBOOLE_0:def 4;
      then consider F1 being set such that
A12:  x in F1 and
A13:  F1 in Fa by A4,TARSKI:def 4;
      reconsider C1=F1 as Subset of GX by A13;
      x in B by A11,XBOOLE_0:def 4;
      then consider F2 being set such that
A14:  x in F2 and
A15:  F2 in Fb by A6,TARSKI:def 4;
      reconsider C2=F2 as Subset of GX by A15;
A16:  C2 is a_component by A5,A15;
      C1 is a_component by A3,A13;
      then
A17:  C1 = C2 or C1 misses C2 by A16,CONNSP_1:35;
      F1 /\ F2 <>{} by A12,A14,XBOOLE_0:def 4;
      then C1 in Fa /\ Fb by A13,A15,A17,XBOOLE_0:def 4,def 7;
      hence thesis by A12,TARSKI:def 4;
    end;
    union Fd c= A /\ B
    proof
      let x be set;
      assume x in union Fd;
      then consider X4 being set such that
A18:  x in X4 and
A19:  X4 in Fd by TARSKI:def 4;
      X4 in Fb by A19,XBOOLE_0:def 4;
      then
A20:  x in union Fb by A18,TARSKI:def 4;
      X4 in Fa by A19,XBOOLE_0:def 4;
      then x in union Fa by A18,TARSKI:def 4;
      hence thesis by A4,A6,A20,XBOOLE_0:def 4;
    end;
    then A /\ B =union Fd by A10,XBOOLE_0:def 10;
    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
  for Fu being Subset-Family of GX st (for A being Subset of GX st A in
  Fu holds A is a_union_of_components of GX) holds union Fu is
  a_union_of_components of GX
proof
  let 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;
    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 being 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 being 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 being 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;
    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 being Subset-Family of GX such that
A6: for B being Subset of GX st B in F holds B is a_component and
A7: B3=union F by Def2;
    consider Y2 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;
    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,XBOOLE_0:def 10;
  hence thesis by A1,Def2;
end;

theorem
  for Fu being Subset-Family of GX st (for A being Subset of GX st A in
  Fu holds A is a_union_of_components of GX) holds meet Fu is
  a_union_of_components of GX
proof
  let Fu be Subset-Family of GX;
  assume
A1: for A being 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;
        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;
        consider Y2 such that
A4:     Y2 in Fu by A2,XBOOLE_0:def 1;
        reconsider B2=Y2 as Subset of GX by A4;
        B2 is a_union_of_components of GX by A1,A4;
        then consider F being Subset-Family of GX such that
A5:     for B being Subset of GX st B in F holds B is a_component and
A6:     B2=union F by Def2;
        assume
A7:     x in meet Fu;
        then x in Y2 by A4,SETFAM_1:def 1;
        then consider Y3 being set such that
A8:     x in Y3 and
A9:     Y3 in F by A6,TARSKI:def 4;
        reconsider B3=Y3 as Subset of GX by A9;
A10:    for A2 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 being 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;
        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,XBOOLE_0:def 10;
      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
  for A,B being Subset of GX st A is a_union_of_components of GX & B is
  a_union_of_components of GX holds A \ B is a_union_of_components of GX
proof
  let 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 being Subset-Family of GX such that
A3: for B2 being Subset of GX st B2 in Fa holds B2 is a_component and
A4: A=union Fa by A1,Def2;
  consider Fb being Subset-Family of GX such that
A5: for B3 being Subset of GX st B3 in Fb holds B3 is a_component and
A6: B=union Fb by A2,Def2;
  reconsider Fd=Fa\Fb as Subset-Family of GX;
A7: union Fd c= A \ B
  proof
    let x;
    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 being set such that
A14:  x in Y3 and
A15:  Y3 in Fb by A6,TARSKI:def 4;
      reconsider B3=Y3 as Subset of GX by A15;
      A2 /\ B3 <>{} by A8,A14,XBOOLE_0:def 4;
      then
A16:  A2 meets B3 by XBOOLE_0:def 7;
      B3 is a_component by A5,A15;
      hence contradiction by A10,A12,A15,A16,CONNSP_1:35;
    end;
    A2 c= A by A4,A11,ZFMISC_1:74;
    hence thesis by A8,A13,XBOOLE_0:def 5;
  end;
A17: for B4 being 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;
    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,XBOOLE_0:def 10;
  hence thesis by A17,Def2;
end;

begin :: Operations Down and Up

definition
  let GX be TopStruct, B be Subset of GX, p be Point of GX;
  assume
A1: p in B;
  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<>{};
  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;
  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;
  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;
  func Component_of(p,B) -> Subset of GX means
  :Def7:
  for q being 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 being Point of GX|B st q=p holds S=Component_of q and
A4: for q2 being Point of GX|B st q2=p holds S9=Component_of q2;
    S=Component_of q3 by A3;
    hence thesis by A4;
  end;
end;

theorem
  for B being 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 Th27:
  for B being 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
  for GX being TopSpace for V,B being Subset of GX st V is open holds
  Down(V,B) is open
proof
  let GX be TopSpace;
  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 Th29:
  for V,B being 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
  for B being Subset of GX,V being 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
  for V,B being 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
  for B being Subset of GX, V being Subset of GX|B st V c= B holds Down(
  Up(V),B)=V by XBOOLE_1:28;

theorem
  for B being 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;

:: Moved from JORDAN1B, AK, 22.02.2006

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
  for T being non empty TopSpace for A being non empty
  a_union_of_components of T st A is connected holds A is a_component
proof
  let T be non empty TopSpace;
  let A be non empty a_union_of_components of T;
  consider F being Subset-Family of T such that
A1: for B being Subset of T st B in F holds B is a_component and
A2: A = union F by Def2;
  consider X being set such that
  X <> {} and
A3: X in F by A2,ORDERS_1:6;
  reconsider X as Subset of T by A3;
  assume
A4: A is connected;
  F={X}
  proof
    thus F c= {X}
    proof
      let x be set;
      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 set;
    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;