The Mizar article:

Separated and Weakly Separated Subspaces of Topological Spaces

by
Zbigniew Karno

Received January 8, 1992

Copyright (c) 1992 Association of Mizar Users

MML identifier: TSEP_1
[ MML identifier index ]


environ

 vocabulary BOOLE, PRE_TOPC, SUBSET_1, RELAT_1, TARSKI, SETFAM_1, CONNSP_1,
      TSEP_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, CONNSP_1, BORSUK_1;
 constructors CONNSP_1, BORSUK_1, MEMBERED;
 clusters PRE_TOPC, BORSUK_1, STRUCT_0, COMPLSP1, SUBSET_1, TOPS_1, MEMBERED,
      ZFMISC_1;
 requirements BOOLE, SUBSET;
 definitions PRE_TOPC;
 theorems PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, BORSUK_1, SUBSET_1, XBOOLE_0,
      XBOOLE_1;

begin

 Lm1: for A being set for B,C,D being Subset of A st B \ C = {}
          holds B misses (D \ C)
  proof let A be set; let B,C,D be Subset of A;
   assume B \ C = {}; then B c= C & C misses (D \ C) by XBOOLE_1:37,79;
   hence thesis by XBOOLE_1:63;
  end;

 Lm2: for A being set for B,C,D being Subset of A st B misses C
          holds B misses (C \ D)
  proof let A be set; let B,C,D be Subset of A;
   assume B misses C; then C \ D c= C & C misses B by XBOOLE_1:36;
   hence thesis by XBOOLE_1:63;
  end;
 Lm3: for A,B,C being set holds (A /\ B) \ C = (A \ C) /\ (B \ C)
  proof let A,B,C be set;
    A1: A \ C c= A by XBOOLE_1:36;
A2: (A \ C) misses C by XBOOLE_1:79;
   thus (A /\ B) \ C = (A \ C) /\ B by XBOOLE_1:49
                   .= (A \ C) \ ((A \ C) \ B) by XBOOLE_1:48
                   .= (A \ C) \ (A \ (C \/ B)) by XBOOLE_1:41
                   .= ((A \ C) \ A) \/ ((A \ C) /\ (C \/ B)) by XBOOLE_1:52
                   .= {} \/ ((A \ C) /\ (C \/ B)) by A1,XBOOLE_1:37
                   .= (A \ C) /\ ((B \ C) \/ C) by XBOOLE_1:39
                   .= (A \ C) /\ (B \ C) \/ (A \ C) /\ C by XBOOLE_1:23
                   .= (A \ C) /\ (B \ C) \/ {} by A2,XBOOLE_0:def 7
                   .= (A \ C) /\ (B \ C);
  end;

::1. Some Properties of Subspaces of Topological Spaces.
reserve X for TopSpace;

theorem Th1:
 for X being TopStruct, X0 being SubSpace of X holds the carrier of X0
   is Subset of X
 proof let X be TopStruct, X0 be SubSpace of X;
  reconsider A = [#]X0 as Subset of [#]X by PRE_TOPC:def 9;
     A c= [#]X & [#]X0 = the carrier of X0 by PRE_TOPC:12;
  hence thesis by PRE_TOPC:16;
 end;

theorem Th2:
 for X being TopStruct holds X is SubSpace of X
 proof
  let X be TopStruct;
  thus [#]X c= [#]X;
  thus for P being Subset of X holds P in the topology of X iff
           ex Q being Subset of X
             st Q in the topology of X & P = Q /\ [#]X
    proof let P be Subset of X;
     thus P in the topology of X implies
       ex Q being Subset of X st
                             Q in the topology of X & P = Q /\ [#]X
        proof assume A1: P in the topology of X;
          take P;
          thus thesis by A1,PRE_TOPC:15;
        end;
     thus thesis by PRE_TOPC:15;
    end;
 end;

theorem
   for X being strict TopStruct holds X|[#]X = X
 proof let X be strict TopStruct;
  reconsider X0 = X as SubSpace of X by Th2;
   reconsider P = [#]X0 as Subset of X;
     X|P = X0 by PRE_TOPC:def 10;
  hence thesis;
 end;

theorem Th4:
 for X1, X2 being SubSpace of X holds
  the carrier of X1 c= the carrier of X2 iff X1 is SubSpace of X2
 proof let X1, X2 be SubSpace of X;
  set A1 = the carrier of X1, A2 = the carrier of X2;
   A1: A1 = [#]X1 & A2 = [#]X2 & (the carrier of X) = [#]X by PRE_TOPC:12;
 thus the carrier of X1 c= the carrier of X2 implies X1 is SubSpace of X2
  proof assume A2: A1 c= A2;
     for P being Subset of X1 holds P in the topology of X1 iff
   ex Q being Subset of X2 st Q in the topology of X2 &
   P = Q /\ A1
    proof let P be Subset of X1;
     thus P in the topology of X1 implies
      ex Q being Subset of X2 st
           Q in the topology of X2 & P = Q /\ A1
      proof assume P in the topology of X1;
       then consider R being Subset of X such that
        A3: R in the topology of X and A4: P = R /\ A1 by A1,PRE_TOPC:def 9;
       reconsider Q = R /\ A2 as Subset of X2 by XBOOLE_1:17;
       take Q;
       thus Q in the topology of X2 by A1,A3,PRE_TOPC:def 9;
          Q /\ A1 = R /\ (A2 /\ A1) by XBOOLE_1:16
              .= R /\ A1 by A2,XBOOLE_1:28;
       hence thesis by A4;
      end;
     given Q being Subset of X2 such that
      A5: Q in the topology of X2 and A6: P = Q /\ A1;
     consider R being Subset of X such that
      A7: R in the topology of X and A8: Q = R /\ [#]X2 by A5,PRE_TOPC:def 9;
          P = R /\ (A2 /\ A1) by A1,A6,A8,XBOOLE_1:16
         .= R /\ A1 by A2,XBOOLE_1:28;
     hence thesis by A1,A7,PRE_TOPC:def 9;
    end;
   hence thesis by A1,A2,PRE_TOPC:def 9;
  end;
  thus X1 is SubSpace of X2 implies the carrier of X1 c= the carrier of X2
                                                      by A1,PRE_TOPC:def 9;
 end;

Lm4:
for X being TopStruct, X0 being SubSpace of X holds
 the TopStruct of X0 is strict SubSpace of X
 proof let X be TopStruct, X0 be SubSpace of X;
   set S = the TopStruct of X0;
    S is SubSpace of X
   proof
     A1: [#](S) = the carrier of S & [#]
(X0) = the carrier of X0 by PRE_TOPC:12;
    hence [#](S) c= [#](X) by PRE_TOPC:def 9;
     let P be Subset of S;
    thus P in
 the topology of S implies ex Q being Subset of X st
                 Q in the topology of X & P = Q /\ [#](S) by A1,PRE_TOPC:def 9;
     given Q being Subset of X such that
         A2: Q in the topology of X & P = Q /\ [#](S);
    thus P in the topology of S by A1,A2,PRE_TOPC:def 9;
   end;
  hence thesis;
 end;

theorem Th5:
 for X being TopStruct
 for X1, X2 being SubSpace of X
   st the carrier of X1 = the carrier of X2
 holds the TopStruct of X1 = the TopStruct of X2
 proof
 let X be TopStruct;
 let X1, X2 be SubSpace of X;
  set A1 = the carrier of X1, A2 = the carrier of X2;
    assume A1: A1 = A2;
    reconsider S1 = the TopStruct of X1, S2 = the TopStruct of X2
                                          as strict SubSpace of X by Lm4;
   A2: A1 = [#]S1 & A2 = [#]S2 by PRE_TOPC:12;
    reconsider A1, A2 as Subset of X by BORSUK_1:35;
      S1 = X|(A1) & X|(A2) = S2 by A2,PRE_TOPC:def 10;
    hence thesis by A1;
 end;

theorem
   for X1, X2 being SubSpace of X st
  X1 is SubSpace of X2 & X2 is SubSpace of X1 holds
   the TopStruct of X1 = the TopStruct of X2
 proof let X1,X2 be SubSpace of X;
   set A1 = the carrier of X1, A2 = the carrier of X2;
  assume X1 is SubSpace of X2 & X2 is SubSpace of X1;
   then A1 c= A2 & A2 c= A1 by Th4;
   then A1 = A2 by XBOOLE_0:def 10;
   hence thesis by Th5;
 end;

theorem Th7:
 for X1 being SubSpace of X for X2 being SubSpace of X1
 holds X2 is SubSpace of X
 proof let X1 be SubSpace of X; let X2 be SubSpace of X1;
   A1: [#]X1 c= [#]X & [#]X2 c= [#]X1 by PRE_TOPC:def 9;
  hence [#](X2) c= [#](X) by XBOOLE_1:1;
  thus for P being Subset of X2 holds P in
 the topology of X2 iff
        ex Q being Subset of X
        st Q in the topology of X & P = Q /\ [#]X2
   proof let P be Subset of X2;
      reconsider P1 = P as Subset of X2;
    thus P in the topology of X2 implies
         ex Q being Subset of X
         st Q in the topology of X & P = Q /\ [#]X2
     proof assume P in the topology of X2;
      then consider R being Subset of X1 such that
      A2: R in the topology of X1 and A3: P = R /\ [#]X2 by PRE_TOPC:def 9;
      consider Q being Subset of X such that
      A4: Q in the topology of X and A5: R = Q /\ [#]X1 by A2,PRE_TOPC:def 9;
        Q /\ [#]X2 = Q /\ ([#]X1 /\ [#]X2) by A1,XBOOLE_1:28
             .= P by A3,A5,XBOOLE_1:16;
      hence thesis by A4;
     end;
      given Q being Subset of X such that
       A6: Q in the topology of X and A7: P = Q /\ [#]X2;
       reconsider Q1 = Q as Subset of X;
       A8: Q1 is open by A6,PRE_TOPC:def 5;
         Q /\ [#]X1 c= [#]X1 & [#]X1 = the carrier of X1 by PRE_TOPC:12,
XBOOLE_1:17;
      then reconsider R = Q /\ [#]X1 as Subset of X1;
       A9: R is open by A8,TOPS_2:32;
         R /\ [#]X2 = Q /\ ([#]X1 /\ [#]X2) by XBOOLE_1:16
              .= P by A1,A7,XBOOLE_1:28;
       then P1 is open by A9,TOPS_2:32;
      hence thesis by PRE_TOPC:def 5;
   end;
 end;

theorem Th8:
 for X0 being SubSpace of X, C, A being Subset of X,
     B being Subset of X0 st
  C is closed & C c= the carrier of X0 & A c= C & A = B holds
   B is closed iff A is closed
 proof
  let X0 be SubSpace of X, C, A be Subset of X,
      B be Subset of X0 such that
 A1: C is closed and A2: C c= the carrier of X0 and A3: A c= C and A4: A = B;
  thus B is closed implies A is closed
   proof assume B is closed;
    then consider F being Subset of X such that
       A5: F is closed and A6: F /\ [#]X0 = B by PRE_TOPC:43;
       [#]X0 = the carrier of X0 by PRE_TOPC:12;
    then A7: F /\ C c= A by A2,A4,A6,XBOOLE_1:26;
       A c= F by A4,A6,XBOOLE_1:17;
    then A c= F /\ C by A3,XBOOLE_1:19;
    then A = F /\ C by A7,XBOOLE_0:def 10;
    hence A is closed by A1,A5,TOPS_1:35;
   end;
  thus A is closed implies B is closed by A4,TOPS_2:34;
 end;

theorem Th9:
 for X0 being SubSpace of X, C, A being Subset of X,
     B being Subset of X0 st
  C is open & C c= the carrier of X0 & A c= C & A = B holds
   B is open iff A is open
 proof
  let X0 be SubSpace of X, C, A be Subset of X,
      B be Subset of X0 such that
 A1: C is open and A2: C c= the carrier of X0 and A3: A c= C and A4: A = B;
  thus B is open implies A is open
   proof assume B is open;
    then consider F being Subset of X such that
       A5: F is open and A6: F /\ [#]X0 = B by TOPS_2:32;
       [#]X0 = the carrier of X0 by PRE_TOPC:12;
    then A7: F /\ C c= A by A2,A4,A6,XBOOLE_1:26;
       A c= F by A4,A6,XBOOLE_1:17;
    then A c= F /\ C by A3,XBOOLE_1:19;
    then A = F /\ C by A7,XBOOLE_0:def 10;
    hence A is open by A1,A5,TOPS_1:38;
   end;
  thus A is open implies B is open by A4,TOPS_2:33;
 end;

theorem Th10:
 for X being non empty TopStruct, A0 being non empty Subset of X
  ex X0 being strict non empty SubSpace of X st A0 = the carrier of X0
 proof let X be non empty TopStruct,
        A0 be non empty Subset of X;
  take X0 = X|A0;
    A0 = [#]X0 by PRE_TOPC:def 10;
  hence thesis by PRE_TOPC:12;
 end;

::Properties of Closed Subspaces (for the definition see BORSUK_1:def 13).
theorem Th11:
 for X0 being SubSpace of X, A being Subset of X
   st A = the carrier of X0 holds
  X0 is closed SubSpace of X iff A is closed
 proof let X0 be SubSpace of X, A be Subset of X;
  assume A1: A = the carrier of X0;
  hence X0 is closed SubSpace of X implies A is closed by BORSUK_1:def 14;
  thus A is closed implies X0 is closed SubSpace of X
   proof assume A is closed;
    then for B be Subset of X
          holds B = the carrier of X0 implies B is closed by A1;
    hence thesis by BORSUK_1:def 14;
   end;
 end;

theorem
   for X0 being closed SubSpace of X,
     A being Subset of X,
     B being Subset of X0
  st A = B holds B is closed iff A is closed
 proof
  let X0 be closed SubSpace of X, A be Subset of X,
      B be Subset of X0 such that
    A1: A = B;
    the carrier of X0 is Subset of X by Th1;
  then reconsider C = the carrier of X0 as Subset of X;
     C is closed by Th11;
  hence thesis by A1,Th8;
 end;

theorem
   for X1 being closed SubSpace of X,
     X2 being closed SubSpace of X1 holds
  X2 is closed SubSpace of X
 proof let X1 be closed SubSpace of X,
           X2 be closed SubSpace of X1;
    now let B be Subset of X;
    A1: the carrier of X2 c= the carrier of X1 by BORSUK_1:35;
   assume A2: B = the carrier of X2;
  then reconsider BB = B as Subset of X1 by A1;
      BB is closed by A2,BORSUK_1:def 14;
   then A3: ex A being Subset of X st
             A is closed & A /\ [#]X1 = BB by PRE_TOPC:43;
     A4: [#]X1 = the carrier of X1 by PRE_TOPC:12;
   then [#]X1 is Subset of X by BORSUK_1:35;
   then reconsider C = [#]X1 as Subset of X;
      C is closed by A4,BORSUK_1:def 14;
   hence B is closed by A3,TOPS_1:35;
  end;
  hence thesis by Th7,BORSUK_1:def 14;
 end;

theorem
   for X being non empty TopSpace, X1 being closed non empty SubSpace of X,
     X2 being non empty SubSpace of X st
  the carrier of X1 c= the carrier of X2 holds
   X1 is closed non empty SubSpace of X2
 proof let X be non empty TopSpace, X1 be closed non empty SubSpace of X,
   X2 be non empty SubSpace of X;
  assume the carrier of X1 c= the carrier of X2;
   then reconsider B = the carrier of X1 as Subset of X2;
    now let C be Subset of X2; assume A1: C = the carrier of X1;
   then C is Subset of X by BORSUK_1:35;
   then reconsider A = C as Subset of X;
     A2: A is closed by A1,Th11;
      [#]X2 = the carrier of X2 by PRE_TOPC:12;
   then A /\ [#]X2 = C by XBOOLE_1:28;
   hence C is closed by A2,PRE_TOPC:43;
  end;
  then B is closed;
  hence thesis by Th4,Th11;
 end;

theorem Th15:
 for X be non empty TopSpace, A0 being non empty Subset of X st A0 is closed
  ex X0 being strict closed non empty SubSpace of X st A0 = the carrier of X0
 proof let X be non empty TopSpace, A0 be non empty Subset of X such that
 A1: A0 is closed;
  consider X0 being strict non empty SubSpace of X such that
   A2: A0 = the carrier of X0 by Th10;
  reconsider Y0 = X0 as strict closed non empty SubSpace of X by A1,A2,Th11;
  take Y0;
  thus thesis by A2;
 end;

definition let X be TopStruct;
  let IT be SubSpace of X;
 attr IT is open means
:Def1: for A being Subset of X st A = the carrier of IT holds A is open;
end;

Lm5:
 for T being TopStruct holds
 the TopStruct of T is SubSpace of T
  proof let T be TopStruct;
    set S = the TopStruct of T;
      [#]S = the carrier of S by PRE_TOPC:12;
   hence [#]S c= [#]T by PRE_TOPC:12;
   let P be Subset of S;
   hereby assume
A1:    P in the topology of S;
     reconsider Q = P as Subset of T;
    take Q;
    thus Q in the topology of T by A1;
    thus P = Q /\ [#]S by PRE_TOPC:15;
   end;
   given Q being Subset of T such that
A2: Q in the topology of T and
A3: P = Q /\ [#]S;
   thus P in the topology of S by A2,A3,PRE_TOPC:15;
  end;

definition let X be TopSpace;
 cluster strict open SubSpace of X;
 existence
  proof
   reconsider Y = the TopStruct of X as strict SubSpace of X by Lm5;
    take Y;
    Y is open
    proof let A be Subset of X;
     assume A = the carrier of Y;
      then A = [#]X by PRE_TOPC:12;
     hence A is open;
    end;
   hence thesis;
  end;
end;

definition let X be non empty TopSpace;
 cluster strict open non empty SubSpace of X;
 existence
  proof
      X|[#]X is open
     proof let A be Subset of X;
      assume A = the carrier of X|[#]X;
      then A = [#](X|[#]X) by PRE_TOPC:12
            .= [#] X by PRE_TOPC:def 10;
      hence A is open;
     end;
   hence thesis;
  end;
end;

::Properties of Open Subspaces.
theorem Th16:
 for X0 being SubSpace of X, A being Subset of X
  st A = the carrier of X0 holds
  X0 is open SubSpace of X iff A is open
 proof let X0 be SubSpace of X, A be Subset of X;
  assume A1: A = the carrier of X0;
  hence X0 is open SubSpace of X implies A is open by Def1;
  thus A is open implies X0 is open SubSpace of X
   proof assume A is open;
    then for B be Subset of X
          holds B = the carrier of X0 implies B is open by A1;
    hence thesis by Def1;
   end;
 end;

theorem
   for X0 being open SubSpace of X, A being Subset of X,
     B being Subset of X0 st
  A = B holds B is open iff A is open
 proof
  let X0 be open SubSpace of X, A be Subset of X,
      B be Subset of X0 such that
    A1: A = B;
     the carrier of X0 is Subset of X by Th1;
   then reconsider C = the carrier of X0 as Subset of X;
     C is open by Th16;
  hence thesis by A1,Th9;
 end;

theorem
   for X1 being open SubSpace of X,
     X2 being open SubSpace of X1 holds
  X2 is open SubSpace of X
 proof let X1 be open SubSpace of X,
           X2 be open SubSpace of X1;
    now let B be Subset of X;
    A1: the carrier of X2 c= the carrier of X1 by BORSUK_1:35;
   assume A2: B = the carrier of X2;
   then reconsider BB = B as Subset of X1 by A1;
      BB is open by A2,Def1;
   then A3: ex A being Subset of X st A is open & A /\ [#]X1 = BB
     by TOPS_2:32;
     A4: [#]X1 = the carrier of X1 by PRE_TOPC:12;
   then [#]X1 is Subset of X by BORSUK_1:35;
   then reconsider C = [#]X1 as Subset of X;
      C is open by A4,Def1;
   hence B is open by A3,TOPS_1:38;
  end;
  hence thesis by Def1,Th7;
 end;

theorem
   for X be non empty TopSpace, X1 being open SubSpace of X,
   X2 being non empty SubSpace of X st
  the carrier of X1 c= the carrier of X2 holds
   X1 is open SubSpace of X2
 proof let X be non empty TopSpace, X1 be open SubSpace of X,
   X2 be non empty SubSpace of X;
  assume the carrier of X1 c= the carrier of X2;
   then reconsider B = the carrier of X1 as Subset of X2;
    now let C be Subset of X2; assume A1: C = the carrier of X1;
   then C is Subset of X by BORSUK_1:35;
   then reconsider A = C as Subset of X;
     A2: A is open by A1,Th16;
      [#]X2 = the carrier of X2 by PRE_TOPC:12;
   then A /\ [#]X2 = C by XBOOLE_1:28;
   hence C is open by A2,TOPS_2:32;
  end;
  then B is open;
  hence thesis by Th4,Th16;
 end;

theorem Th20:
 for X be non empty TopSpace, A0 being non empty Subset of X st A0 is open
  ex X0 being strict open non empty SubSpace of X st A0 = the carrier of X0
 proof let X be non empty TopSpace, A0 be non empty Subset of X such that
A1: A0 is open;
  consider X0 being strict non empty SubSpace of X such that
    A2: A0 = the carrier of X0 by Th10;
   reconsider Y0 = X0 as strict open non empty SubSpace of X by A1,A2,Th16;
  take Y0;
  thus thesis by A2;
 end;


begin
::2. Operations on Subspaces of Topological Spaces.
reserve X for non empty TopSpace;

definition let X be non empty TopStruct;
           let X1, X2 be non empty SubSpace of X;
  func X1 union X2 -> strict non empty SubSpace of X means
 :Def2: the carrier of it = (the carrier of X1) \/ (the carrier of X2);
 existence
  proof
   reconsider A1 = the carrier of X1,
              A2 = the carrier of X2 as Subset of X by Th1;
   set A = A1 \/ A2;
    reconsider A as non empty Subset of X by XBOOLE_1:15;
   take X|A;
   thus the carrier of (X|A) = [#](X|A) by PRE_TOPC:12
        .= (the carrier of X1) \/ (the carrier of X2) by PRE_TOPC:def 10;
  end;
 uniqueness by Th5;
 commutativity;
end;

reserve X1, X2, X3 for non empty SubSpace of X;

::Properties of the Union of two Subspaces.
theorem
    (X1 union X2) union X3 = X1 union (X2 union X3)
 proof
      the carrier of (X1 union X2) union X3 =
         (the carrier of X1 union X2) \/ (the carrier of X3) by Def2
      .= ((the carrier of X1) \/ (the carrier of X2)) \/ (the carrier of X3)
                                                                   by Def2
      .= (the carrier of X1) \/ ((the carrier of X2) \/ (the carrier of X3))
                                                                   by XBOOLE_1:
4
      .= (the carrier of X1) \/ (the carrier of X2 union X3) by Def2
      .= the carrier of X1 union (X2 union X3) by Def2;
    hence thesis by Th5;
 end;

theorem Th22:
 X1 is SubSpace of X1 union X2
 proof
  set A1 = the carrier of X1, A2 = the carrier of X2,
       A = the carrier of X1 union X2;
     A = A1 \/ A2 by Def2;
  then A1 c= A & A2 c= A by XBOOLE_1:7;
  hence thesis by Th4;
 end;

theorem
   for X1,X2 being non empty SubSpace of X holds
  X1 is SubSpace of X2 iff X1 union X2 = the TopStruct of X2
 proof let X1,X2 be non empty SubSpace of X;
  set A1 = the carrier of X1, A2 = the carrier of X2;
  thus X1 is SubSpace of X2 iff X1 union X2 = the TopStruct of X2
   proof
    thus X1 is SubSpace of X2 implies X1 union X2 = the TopStruct of X2
     proof assume X1 is SubSpace of X2;
      then A1 c= A2 by BORSUK_1:35;
      then A1 \/ A2 = the carrier of the TopStruct of X2 &
        the TopStruct of X2 is strict SubSpace of X by Lm4,XBOOLE_1:12;
      hence thesis by Def2;
     end;
    assume X1 union X2 = the TopStruct of X2;
    then A1 \/ A2 = A2 by Def2;
    then A1 c= A2 by XBOOLE_1:7;
    hence X1 is SubSpace of X2 by Th4;
   end;
 end;

theorem
   for X1, X2 being closed non empty SubSpace of X holds
  X1 union X2 is closed SubSpace of X
 proof let X1, X2 be closed non empty SubSpace of X;
     the carrier of X1 is Subset of X by Th1;
   then reconsider A1 = the carrier of X1 as Subset of X
   ;
     the carrier of X2 is Subset of X by Th1;
   then reconsider A2 = the carrier of X2 as Subset of X
   ;
     the carrier of X1 union X2 is Subset of X by Th1;
   then reconsider A = the carrier of X1 union X2 as Subset of X
    ;
      A1 is closed & A2 is closed by Th11;
  then A1 \/ A2 is closed by TOPS_1:36;
  then A is closed by Def2;
  hence thesis by Th11;
 end;

theorem
   for X1, X2 being open non empty SubSpace of X holds
  X1 union X2 is open SubSpace of X
 proof let X1, X2 be open non empty SubSpace of X;
     the carrier of X1 is Subset of X by Th1;
   then reconsider A1 = the carrier of X1 as Subset of X
   ;
     the carrier of X2 is Subset of X by Th1;
   then reconsider A2 = the carrier of X2 as Subset of X
   ;
     the carrier of X1 union X2 is Subset of X by Th1;
   then reconsider A = the carrier of X1 union X2 as Subset of X
   ;
      A1 is open & A2 is open by Th16;
  then A1 \/ A2 is open by TOPS_1:37;
  then A is open by Def2;
  hence thesis by Th16;
 end;

definition let X be TopStruct; let X1, X2 be SubSpace of X;
  pred X1 misses X2 means
 :Def3: the carrier of X1 misses the carrier of X2;
 correctness;
 symmetry;
 antonym X1 meets X2;
end;

definition let X be non empty TopStruct; let X1, X2 be non empty SubSpace of X;
  assume A1: X1 meets X2;
 canceled;

  func X1 meet X2 -> strict non empty SubSpace of X means
 :Def5: the carrier of it = (the carrier of X1) /\ (the carrier of X2);
 existence
  proof
    reconsider A1 = the carrier of X1, A2 = the carrier of X2
      as Subset of X by Th1;
    set A = A1 /\ A2;
      A1 meets A2 by A1,Def3;
    then reconsider A as non empty Subset of X
      by XBOOLE_0:def 7;
   take X|A;
   thus the carrier of (X|A) = [#](X|A) by PRE_TOPC:12
      .= (the carrier of X1) /\ (the carrier of X2) by PRE_TOPC:def 10;
  end;
 uniqueness by Th5;
end;

reserve X1, X2, X3 for non empty SubSpace of X;

::Properties of the Meet of two Subspaces.
canceled 3;

theorem Th29:
 (X1 meets X2 implies X1 meet X2 = X2 meet X1) &
  ((X1 meets X2 & (X1 meet X2) meets X3 or X2 meets X3 & X1 meets (X2 meet X3))
    implies (X1 meet X2) meet X3 = X1 meet (X2 meet X3))
 proof
  thus X1 meets X2 implies X1 meet X2 = X2 meet X1
   proof assume
A1:    X1 meets X2;
    then the carrier of X1 meet X2 =(the carrier of X2) /\ (the carrier of X1)
 by Def5
      .= the carrier of X2 meet X1 by A1,Def5;
    hence thesis by Th5;
   end;
    now assume A2:
    X1 meets X2 & (X1 meet X2) meets X3 or X2 meets X3 & X1 meets (X2 meet X3);
   A3: now assume A4: X1 meets X2 & (X1 meet X2) meets X3;
        then (the carrier of X1 meet X2) meets (the carrier of X3) by Def3;
        then (the carrier of X1 meet X2) /\ (the carrier of X3) <> {}
          by XBOOLE_0:def 7;
        then ((the carrier of X1) /\ (the carrier of X2)) /\
          (the carrier of X3) <> {} by A4,Def5;
then A5: (the carrier of X1) /\ ((the carrier of X2) /\ (the carrier of X3)) <>
{}
                                                                  by XBOOLE_1:
16;
        then (the carrier of X2) /\ (the carrier of X3) <> {};
        then A6: (the carrier of X2) meets (the carrier of X3) by XBOOLE_0:def
7;
        then X2 meets X3 by Def3;
        then (the carrier of X1) /\ (the carrier of X2 meet X3) <> {}
 by A5,Def5;
        then (the carrier of X1) meets (the carrier of X2 meet X3)
         by XBOOLE_0:def 7;
        hence X1 meets X2 & (X1 meet X2) meets X3
              & X2 meets X3 & X1 meets (X2 meet X3) by A4,A6,Def3;
       end;
   A7: now assume A8: X2 meets X3 & X1 meets (X2 meet X3);
        then (the carrier of X1) meets (the carrier of X2 meet X3) by Def3;
        then (the carrier of X1) /\ (the carrier of X2 meet X3) <> {}
          by XBOOLE_0:def 7;
         then (the carrier of X1) /\ ((the carrier of X2) /\
 (the carrier of X3)) <> {} by A8,Def5;
then A9: ((the carrier of X1) /\ (the carrier of X2)) /\ (the carrier of X3) <>
{}
                                                      by XBOOLE_1:16;
     then (the carrier of X1) /\ (the carrier of X2) <> {};
then A10: (the carrier of X1) meets (the carrier of X2) by XBOOLE_0:def 7;
        then X1 meets X2 by Def3;
        then (the carrier of X1 meet X2) /\ (the carrier of X3) <> {}
 by A9,Def5;
        then (the carrier of X1 meet X2) meets (the carrier of X3)
         by XBOOLE_0:def 7;
        hence X1 meets X2 & (X1 meet X2) meets X3
              & X2 meets X3 & X1 meets (X2 meet X3) by A8,A10,Def3;
       end;
    then the carrier of (X1 meet X2) meet X3 =
         (the carrier of X1 meet X2) /\ (the carrier of X3) by A2,Def5
      .= ((the carrier of X1) /\ (the carrier of X2)) /\ (the carrier of X3)
                                                           by A2,A7,Def5
      .= (the carrier of X1) /\ ((the carrier of X2) /\ (the carrier of X3))
                                                                 by XBOOLE_1:16
      .= (the carrier of X1) /\ (the carrier of X2 meet X3) by A2,A3,Def5
      .= the carrier of X1 meet (X2 meet X3) by A2,A3,Def5;
    hence (X1 meet X2) meet X3 = X1 meet (X2 meet X3) by Th5;
  end;
  hence thesis;
 end;

theorem Th30:
 X1 meets X2 implies
  X1 meet X2 is SubSpace of X1 & X1 meet X2 is SubSpace of X2
 proof assume X1 meets X2;
  then the carrier of X1 meet X2 = (the carrier of X1) /\ (the carrier of X2)
                                                                    by Def5;
  then the carrier of X1 meet X2 c= the carrier of X1
      & the carrier of X1 meet X2 c= the carrier of X2 by XBOOLE_1:17;
  hence thesis by Th4;
 end;

theorem
   for X1,X2 being non empty SubSpace of X holds
  X1 meets X2 implies
   (X1 is SubSpace of X2 iff X1 meet X2 = the TopStruct of X1) &
    (X2 is SubSpace of X1 iff X1 meet X2 = the TopStruct of X2)
 proof let X1,X2 be non empty SubSpace of X;
  assume A1: X1 meets X2;
  set A1 = the carrier of X1, A2 = the carrier of X2;
  thus X1 is SubSpace of X2 iff X1 meet X2 = the TopStruct of X1
   proof
    thus X1 is SubSpace of X2 implies X1 meet X2 = the TopStruct of X1
     proof assume X1 is SubSpace of X2;
      then A1 c= A2 by BORSUK_1:35;
      then A1 /\ A2 = the carrier of the TopStruct of X1 &
        the TopStruct of X1 is strict SubSpace of X by Lm4,XBOOLE_1:28;
      hence thesis by A1,Def5;
     end;
    assume X1 meet X2 = the TopStruct of X1;
    then A1 /\ A2 = A1 by A1,Def5;
    then A1 c= A2 by XBOOLE_1:17;
    hence X1 is SubSpace of X2 by Th4;
   end;
  thus X2 is SubSpace of X1 iff X1 meet X2 = the TopStruct of X2
   proof
    thus X2 is SubSpace of X1 implies X1 meet X2 = the TopStruct of X2
     proof assume X2 is SubSpace of X1;
      then A2 c= A1 by BORSUK_1:35;
      then A1 /\ A2 = the carrier of the TopStruct of X2 &
        the TopStruct of X2 is strict SubSpace of X by Lm4,XBOOLE_1:28;
      hence thesis by A1,Def5;
     end;
    assume X1 meet X2 = the TopStruct of X2;
    then A1 /\ A2 = A2 by A1,Def5;
    then A2 c= A1 by XBOOLE_1:17;
    hence X2 is SubSpace of X1 by Th4;
   end;
 end;

theorem
   for X1, X2 being closed non empty SubSpace of X st X1 meets X2 holds
  X1 meet X2 is closed SubSpace of X
 proof let X1, X2 be closed non empty SubSpace of X such that A1: X1 meets X2;
      the carrier of X1 is Subset of X by Th1;
    then reconsider A1 = the carrier of X1 as Subset of X
    ;
      the carrier of X2 is Subset of X by Th1;
    then reconsider A2 = the carrier of X2 as Subset of X
    ;
      the carrier of X1 meet X2 is Subset of X by Th1;
    then reconsider A = the carrier of X1 meet X2 as Subset of X
     ;
     A1 is closed & A2 is closed by Th11;
  then A1 /\ A2 is closed by TOPS_1:35;
  then A is closed by A1,Def5;
  hence thesis by Th11;
 end;

theorem
   for X1, X2 being open non empty SubSpace of X st X1 meets X2 holds
  X1 meet X2 is open SubSpace of X
 proof let X1, X2 be open non empty SubSpace of X such that A1: X1 meets X2;
      the carrier of X1 is Subset of X by Th1;
    then reconsider A1 = the carrier of X1 as Subset of X
    ;
      the carrier of X2 is Subset of X by Th1;
    then reconsider A2 = the carrier of X2 as Subset of X
    ;
      the carrier of X1 meet X2 is Subset of X by Th1;
    then reconsider A = the carrier of X1 meet X2 as Subset of X
     ;
     A1 is open & A2 is open by Th16;
  then A1 /\ A2 is open by TOPS_1:38;
  then A is open by A1,Def5;
  hence thesis by Th16;
 end;

::Connections between the Union and the Meet.
theorem
   X1 meets X2 implies
  X1 meet X2 is SubSpace of X1 union X2
 proof assume X1 meets X2;
  then A1: X1 meet X2 is SubSpace of X1 by Th30;
     X1 is SubSpace of X1 union X2 by Th22;
  hence thesis by A1,Th7;
 end;

theorem
   for Y being non empty SubSpace of X st
  X1 meets Y & Y meets X2 holds
   (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y) &
     Y meet (X1 union X2) = (Y meet X1) union (Y meet X2)
 proof let Y be non empty SubSpace of X;
   assume A1: X1 meets Y & Y meets X2;
     X1 is SubSpace of X1 union X2 by Th22;
  then the carrier of X1 c= the carrier of X1 union X2 by Th4;
  then (the carrier of X1) /\ (the carrier of Y) c=
       (the carrier of X1 union X2) /\ (the carrier of Y) &
       (the carrier of X1) meets (the carrier of Y) by A1,Def3,XBOOLE_1:26;
  then (the carrier of X1) /\ (the carrier of Y) c=
       (the carrier of X1 union X2) /\ (the carrier of Y) &
       (the carrier of X1) /\ (the carrier of Y) <> {} by XBOOLE_0:def 7;
  then (the carrier of X1 union X2) /\ (the carrier of Y) <> {} by XBOOLE_1:3;
  then (the carrier of X1 union X2) meets (the carrier of Y) by XBOOLE_0:def 7
;
  then A2: (X1 union X2) meets Y by Def3;
  thus (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y)
   proof
      the carrier of (X1 union X2) meet Y =
         (the carrier of X1 union X2) /\ (the carrier of Y) by A2,Def5
      .= ((the carrier of X1) \/ (the carrier of X2)) /\ (the carrier of Y)
                                                               by Def2
      .= ((the carrier of X1) /\ (the carrier of Y)) \/
         ((the carrier of X2) /\ (the carrier of Y)) by XBOOLE_1:23
      .= (the carrier of X1 meet Y) \/
         ((the carrier of X2) /\ (the carrier of Y)) by A1,Def5
      .= (the carrier of X1 meet Y) \/ (the carrier of X2 meet Y) by A1,Def5
      .= the carrier of (X1 meet Y) union (X2 meet Y) by Def2;
    hence thesis by Th5;
   end;
  hence Y meet (X1 union X2) = (X1 meet Y) union (X2 meet Y) by A2,Th29
                           .= (Y meet X1) union (X2 meet Y) by A1,Th29
                           .= (Y meet X1) union (Y meet X2) by A1,Th29;
 end;

theorem
   for Y being non empty SubSpace of X holds X1 meets X2 implies
  (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) &
    Y union (X1 meet X2) = (Y union X1) meet (Y union X2)
 proof let Y be non empty SubSpace of X;
  assume A1: X1 meets X2;
     Y is SubSpace of X1 union Y & Y is SubSpace of X2 union Y by Th22;
  then the carrier of Y c= the carrier of X1 union Y &
       the carrier of Y c= the carrier of X2 union Y by Th4;
  then the carrier of Y c=
      (the carrier of X1 union Y) /\ (the carrier of X2 union Y) &
       the carrier of Y <> {} by XBOOLE_1:19;
  then (the carrier of X1 union Y) /\ (the carrier of X2 union Y) <> {}
                                                               by XBOOLE_1:3;
  then (the carrier of X1 union Y) meets (the carrier of X2 union Y)
                                                             by XBOOLE_0:def 7;
  then A2: (X1 union Y) meets (X2 union Y) by Def3;
  thus (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y)
   proof
      the carrier of (X1 meet X2) union Y =
         (the carrier of X1 meet X2) \/ (the carrier of Y) by Def2
      .= ((the carrier of X1) /\ (the carrier of X2)) \/ (the carrier of Y)
                                                               by A1,Def5
      .= ((the carrier of X1) \/ (the carrier of Y)) /\
         ((the carrier of X2) \/ (the carrier of Y)) by XBOOLE_1:24
      .= (the carrier of X1 union Y) /\
         ((the carrier of X2) \/ (the carrier of Y)) by Def2
      .= (the carrier of X1 union Y) /\ (the carrier of X2 union Y) by Def2
      .= the carrier of (X1 union Y) meet (X2 union Y) by A2,Def5;
    hence thesis by Th5;
   end;
  hence Y union (X1 meet X2) = (Y union X1) meet (Y union X2);
 end;


begin
::3. Separated and Weakly Separated Subsets of Topological Spaces.

definition let X be TopStruct, A1, A2 be Subset of X;
 redefine    ::for the previous definition see CONNSP_1:def 1
  pred A1,A2 are_separated;
 antonym A1,A2 are_not_separated;
end;

reserve X for TopSpace;
reserve A1, A2 for Subset of X;

::Properties of Separated Subsets of Topological Spaces.
theorem Th37:
 for A1,A2 being Subset of X holds
  A1,A2 are_separated implies A1 misses A2 by CONNSP_1:2;

theorem Th38:
 A1 is closed & A2 is closed implies (A1 misses A2 iff A1,A2 are_separated)
 proof assume A1: A1 is closed & A2 is closed;
  thus A1 misses A2 implies A1,A2 are_separated
   proof assume A2: A1 misses A2;
      Cl A1 = A1 & Cl A2 = A2 by A1,PRE_TOPC:52;
    hence thesis by A2,CONNSP_1:def 1;
   end;
  thus A1,A2 are_separated implies A1 misses A2 by CONNSP_1:2;
 end;

theorem Th39:
 A1 \/ A2 is closed & A1,A2 are_separated implies A1 is closed & A2 is closed
 proof assume A1: A1 \/ A2 is closed;
     A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7;
  then Cl A1 c= A1 \/ A2 & Cl A2 c= A1 \/ A2 by A1,TOPS_1:31;
  then A2: Cl A1 \ A2 c= A1 & Cl A2 \ A1 c= A2 by XBOOLE_1:43;
   assume A1,A2 are_separated;
  then Cl A1 misses A2 & Cl A2 misses A1 by CONNSP_1:def 1;
  then Cl A2 c= A2 & Cl A1 c= A1 & A1 c= Cl A1 & A2 c= Cl A2
                                               by A2,PRE_TOPC:48,XBOOLE_1:83;
  hence thesis by XBOOLE_0:def 10;
 end;

theorem Th40:
 A1 misses A2 & A1 is open implies A1 misses Cl A2
 proof assume A1:A1 misses A2;
  thus A1 is open implies A1 misses Cl A2
   proof assume A1 is open;
    then A2 c= A1` & A1` is closed by A1,PRE_TOPC:21,TOPS_1:30;
    then Cl A2 c= A1` by TOPS_1:31;
    then Cl A2 misses A1`` by TOPS_1:20;
    then Cl A2 /\ A1`` = {} by XBOOLE_0:def 7;
    then Cl A2 /\ A1 = {};
    hence thesis by XBOOLE_0:def 7;
   end;
 end;

theorem Th41:
 A1 is open & A2 is open implies (A1 misses A2 iff A1,A2 are_separated)
 proof assume A1: A1 is open & A2 is open;
  thus A1 misses A2 implies A1,A2 are_separated
   proof assume A1 misses A2;
    then A1 misses Cl A2 & Cl A1 misses A2 by A1,Th40;
    hence thesis by CONNSP_1:def 1;
   end;
  thus A1,A2 are_separated implies A1 misses A2 by CONNSP_1:2;
 end;

theorem Th42:
 A1 \/ A2 is open & A1,A2 are_separated implies A1 is open & A2 is open
 proof assume A1: A1 \/ A2 is open;
    A2: A1 c= Cl A1 & A2 c= Cl A2 by PRE_TOPC:48;
   assume A1,A2 are_separated;
  then A2 misses Cl A1 & A1 misses Cl A2 by CONNSP_1:def 1;
  then A3: A2 c= (Cl A1)` & A1 c= (Cl A2)` by PRE_TOPC:21;
   A4: (A1 \/ A2) /\ (Cl A1)` = (A1 \/ A2) \ Cl A1 by SUBSET_1:32
                           .= (A1 \ Cl A1) \/ (A2 \ Cl A1) by XBOOLE_1:42
                           .= {} \/ (A2 \ Cl A1) by A2,XBOOLE_1:37
                           .= A2 /\ (Cl A1)` by SUBSET_1:32
                           .= A2 by A3,XBOOLE_1:28;
     (A1 \/ A2) /\ (Cl A2)` = (A1 \/ A2) \ Cl A2 by SUBSET_1:32
                           .= (A1 \ Cl A2) \/ (A2 \ Cl A2) by XBOOLE_1:42
                           .= (A1 \ Cl A2) \/ {} by A2,XBOOLE_1:37
                           .= A1 /\ (Cl A2)` by SUBSET_1:32
                           .= A1 by A3,XBOOLE_1:28;
  hence thesis by A1,A4,TOPS_1:38;
 end;

::A Restriction Theorem for Separated Subsets (see also CONNSP_1:8).
reserve A1,A2 for Subset of X;

theorem Th43:
 for C being Subset of X holds
  A1,A2 are_separated implies
  A1 /\ C,A2 /\ C are_separated
 proof let C be Subset of X;
  assume A1: A1,A2 are_separated;
       A1 /\ C c= A1 & A2 /\ C c= A2 by XBOOLE_1:17;
    hence thesis by A1,CONNSP_1:8;
 end;

theorem Th44:
 for B being Subset of X holds
   A1,B are_separated or A2,B are_separated implies A1 /\ A2,B are_separated
 proof let B be Subset of X;
  thus
     A1,B are_separated or A2,B are_separated implies A1 /\ A2,B are_separated
   proof assume A1: A1,B are_separated or A2,B are_separated;
    A2: now assume A3: A1,B are_separated;
           A1 /\ A2 c= A1 by XBOOLE_1:17;
        hence A1 /\ A2,B are_separated by A3,CONNSP_1:8;
       end;
         now assume A4: A2,B are_separated;
           A1 /\ A2 c= A2 by XBOOLE_1:17;
        hence A1 /\ A2,B are_separated by A4,CONNSP_1:8;
       end;
    hence thesis by A1,A2;
   end;
 end;

theorem Th45:
 for B being Subset of X holds
  A1,B are_separated & A2,B are_separated iff A1 \/ A2,B are_separated
 proof let B be Subset of X;
  thus A1,B are_separated & A2,B are_separated iff A1 \/ A2,B are_separated
   proof
    thus
        A1,B are_separated & A2,B are_separated implies A1 \/ A2,B
are_separated
         by CONNSP_1:9;
    thus
        A1 \/ A2,B are_separated implies A1,B are_separated & A2,B
are_separated
     proof assume A1: A1 \/ A2,B are_separated;
        A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7;
      hence thesis by A1,CONNSP_1:8;
     end;
   end;
 end;

theorem Th46:
 A1,A2 are_separated iff
  ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
   C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed
 proof
  thus A1,A2 are_separated implies
    ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
     C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed
   proof
     set C1 = Cl A1, C2 = Cl A2;
    assume A1: A1,A2 are_separated;
    take C1,C2;
    thus thesis by A1,CONNSP_1:def 1,PRE_TOPC:48;
   end;
  given C1, C2 being Subset of X such that
   A2: A1 c= C1 & A2 c= C2 and A3: C1 misses A2 & C2 misses A1 and
   A4: C1 is closed & C2 is closed;
     Cl A1 c= C1 & Cl A2 c= C2 & A2 misses C1 & A1 misses C2
                                           by A2,A3,A4,TOPS_1:31;
  then Cl A1 misses A2 & A1 misses Cl A2 by XBOOLE_1:63;
  hence A1,A2 are_separated by CONNSP_1:def 1;
 end;

::First Characterization of Separated Subsets of Topological Spaces.
theorem Th47:
 A1,A2 are_separated iff
  ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
   C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed
 proof
  thus A1,A2 are_separated implies
    ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
     C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed
   proof assume A1,A2 are_separated;
    then consider C1, C2 being Subset of X such that
     A1: A1 c= C1 & A2 c= C2 and A2: C1 misses A2 & C2 misses A1 and
     A3: C1 is closed & C2 is closed by Th46;
    take C1,C2;
        A1 misses C2 & A2 misses C1 & C1 /\ C2 c= C1 & C1 /\ C2 c= C2
                                                     by A2,XBOOLE_1:17;
     then C1 /\ C2 misses A1 & C1 /\ C2 misses A2 by XBOOLE_1:63;
    hence thesis by A1,A3,XBOOLE_1:70;
   end;
  given C1, C2 being Subset of X such that
   A4: A1 c= C1 & A2 c= C2 and A5: C1 /\ C2 misses A1 \/ A2 and
   A6: C1 is closed & C2 is closed;
    ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
   C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed
   proof
    take C1,C2;
  A7: now assume C1 meets A2;
      then A8: C1 /\ A2 <> {} by XBOOLE_0:def 7;
        C1 /\ A2 c= C1 /\ C2 & C1 /\ A2 c= A2 & A2 c= A1 \/
 A2 by A4,XBOOLE_1:7,17,26;
      then C1 /\ A2 c= (C1 /\ C2) /\ A2 & (C1 /\ C2) /\ A2 c= (C1 /\ C2) /\
 (A1 \/ A2)
                                                               by XBOOLE_1:19,
26;
      then C1 /\ A2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:1;
      then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A8,XBOOLE_1:3;
      hence contradiction by A5,XBOOLE_0:def 7;
     end;
       now assume C2 meets A1;
      then A9: A1 /\ C2 <> {} by XBOOLE_0:def 7;
        A1 /\ C2 c= C1 /\ C2 & A1 /\ C2 c= A1 & A1 c= A1 \/
 A2 by A4,XBOOLE_1:7,17,26;
      then A1 /\ C2 c= (C1 /\ C2) /\ A1 & (C1 /\ C2) /\ A1 c= (C1 /\ C2) /\
 (A1 \/ A2)
                                                               by XBOOLE_1:19,
26;
      then A1 /\ C2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:1;
      then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A9,XBOOLE_1:3;
      hence contradiction by A5,XBOOLE_0:def 7;
     end;
    hence thesis by A4,A6,A7;
   end;
  hence A1,A2 are_separated by Th46;
 end;

theorem Th48:
 A1,A2 are_separated iff
  ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
   C1 misses A2 & C2 misses A1 & C1 is open & C2 is open
 proof
  thus A1,A2 are_separated implies
    ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
     C1 misses A2 & C2 misses A1 & C1 is open & C2 is open
   proof assume A1,A2 are_separated;
    then consider C1, C2 being Subset of X such that
     A1: A1 c= C1 & A2 c= C2 and A2: C1 misses A2 & C2 misses A1 and
     A3: C1 is closed & C2 is closed by Th46;
    take C2`,C1`;
    thus thesis by A1,A2,A3,PRE_TOPC:21,TOPS_1:20,29;
   end;
  given C1, C2 being Subset of X such that
   A4: A1 c= C1 & A2 c= C2 and A5: C1 misses A2 & C2 misses A1 and
   A6: C1 is open & C2 is open;
    ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
   C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed
   proof
    take C2`,C1`;
    thus thesis by A4,A5,A6,PRE_TOPC:21,TOPS_1:20,30;
   end;
  hence A1,A2 are_separated by Th46;
 end;

::Second Characterization of Separated Subsets of Topological Spaces.
theorem Th49:
 A1,A2 are_separated iff
  ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
   C1 /\ C2 misses A1 \/ A2 & C1 is open & C2 is open
 proof
  thus A1,A2 are_separated implies
    ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
     C1 /\ C2 misses A1 \/ A2 & C1 is open & C2 is open
   proof assume A1,A2 are_separated;
    then consider C1, C2 being Subset of X such that
     A1: A1 c= C1 & A2 c= C2 and A2: C1 misses A2 & C2 misses A1 and
     A3: C1 is open & C2 is open by Th48;
    take C1,C2;
        A1 misses C2 & A2 misses C1 & C1 /\ C2 c= C1 & C1 /\ C2 c= C2
                                                     by A2,XBOOLE_1:17;
     then C1 /\ C2 misses A1 & C1 /\ C2 misses A2 by XBOOLE_1:63;
    hence thesis by A1,A3,XBOOLE_1:70;
   end;
  given C1, C2 being Subset of X such that
   A4: A1 c= C1 & A2 c= C2 and A5: C1 /\ C2 misses A1 \/ A2 and
   A6: C1 is open & C2 is open;
    ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
   C1 misses A2 & C2 misses A1 & C1 is open & C2 is open
   proof
    take C1,C2;
  A7: now assume C1 meets A2;
       then A8: C1 /\ A2 <> {} by XBOOLE_0:def 7;
        C1 /\ A2 c= C1 /\ C2 & C1 /\ A2 c= A2 & A2 c= A1 \/
 A2 by A4,XBOOLE_1:7,17,26;
      then C1 /\ A2 c= (C1 /\ C2) /\ A2 & (C1 /\ C2) /\ A2 c= (C1 /\ C2) /\
       (A1 \/ A2) by XBOOLE_1:19,26;
      then C1 /\ A2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:1;
      then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A8,XBOOLE_1:3;
      hence contradiction by A5,XBOOLE_0:def 7;
     end;
       now assume C2 meets A1;
       then A9: A1 /\ C2 <> {} by XBOOLE_0:def 7;
        A1 /\ C2 c= C1 /\ C2 & A1 /\ C2 c= A1 & A1 c= A1 \/
       A2 by A4,XBOOLE_1:7,17,26;
      then A1 /\ C2 c= (C1 /\ C2) /\ A1 & (C1 /\ C2) /\ A1 c= (C1 /\ C2) /\
       (A1 \/ A2) by XBOOLE_1:19,26;
      then A1 /\ C2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:1;
      then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A9,XBOOLE_1:3;
      hence contradiction by A5,XBOOLE_0:def 7;
     end;
    hence thesis by A4,A6,A7;
   end;
  hence A1,A2 are_separated by Th48;
 end;

definition let X be TopStruct, A1, A2 be Subset of X;
 canceled;

   pred A1,A2 are_weakly_separated means
:Def7: A1 \ A2,A2 \ A1 are_separated;
 symmetry;
 antonym A1,A2 are_not_weakly_separated;
end;

reserve X for TopSpace, A1, A2 for Subset of X;

::Properties of Weakly Separated Subsets of Topological Spaces.
canceled;

theorem Th51:
 A1 misses A2 & A1,A2 are_weakly_separated iff A1,A2 are_separated
 proof
  thus A1 misses A2 & A1,A2 are_weakly_separated implies A1,A2 are_separated
   proof
      assume A1: A1 misses A2 & A1,A2 are_weakly_separated;
    then A1 \ A2 = A1 & A2 \ A1 = A2 by XBOOLE_1:83;
    hence A1,A2 are_separated by A1,Def7;
   end;
  assume A2: A1,A2 are_separated;
   then A1 misses A2 by CONNSP_1:2;
   then A1 \ A2 = A1 & A2 \ A1 = A2 by XBOOLE_1:83;
  hence A1 misses A2 & A1,A2 are_weakly_separated by A2,Def7,CONNSP_1:2;
 end;

theorem Th52:
 A1 c= A2 implies A1,A2 are_weakly_separated
 proof assume A1: A1 c= A2;
     now assume A1 c= A2;
       then A2: A1 \ A2 = {} & {}X = {} by XBOOLE_1:37;
      then Cl(A1 \ A2) = {} by PRE_TOPC:52;
      then Cl(A1 \ A2) /\ (A2 \ A1) = {} & (A1 \ A2) /\ Cl(A2 \ A1) = {}
                                                               by A2;
      then Cl(A1 \ A2) misses (A2 \ A1) & (A1 \ A2) misses Cl(A2 \ A1)
                                                        by XBOOLE_0:def 7;
      then A1 \ A2,A2 \ A1 are_separated by CONNSP_1:def 1;
      hence thesis by Def7;
     end;
  hence thesis by A1;
 end;

theorem Th53:
 for A1,A2 being Subset of X holds
  A1 is closed & A2 is closed implies A1,A2 are_weakly_separated
 proof
   let A1,A2 be Subset of X;
   assume A1: A1 is closed & A2 is closed;
     A1 \ A2 c= A1 & A2 \ A1 c= A2 by XBOOLE_1:36;
  then Cl(A1 \ A2) c= A1 & Cl(A2 \ A1) c= A2 by A1,TOPS_1:31;
   then Cl(A1 \ A2) \ A1 = {} & Cl(A2 \ A1) \ A2 = {} by XBOOLE_1:37;
  then Cl(A1 \ A2) misses (A2 \ A1) &
       (A1 \ A2) misses Cl(A2 \ A1) by Lm1;
  then A1 \ A2,A2 \ A1 are_separated by CONNSP_1:def 1;
  hence A1,A2 are_weakly_separated by Def7;
 end;

theorem Th54:
 for A1,A2 being Subset of X holds
  A1 is open & A2 is open implies A1,A2 are_weakly_separated
 proof
  let A1,A2 be Subset of X;
  assume A1: A1 is open & A2 is open;
    A2 misses (A1 \ A2) & (A2 \ A1) misses A1 by XBOOLE_1:79;
  then A2 misses Cl(A1 \ A2) & Cl(A2 \ A1) misses A1 by A1,Th40;
  then Cl(A1 \ A2) misses (A2 \ A1) &
       (A1 \ A2) misses Cl(A2 \ A1) by Lm2;
  then A1 \ A2,A2 \ A1 are_separated by CONNSP_1:def 1;
  hence A1,A2 are_weakly_separated by Def7;
 end;

::Extension Theorems for Weakly Separated Subsets.
theorem Th55:
 for C being Subset of X holds
  A1,A2 are_weakly_separated implies
   A1 \/ C,A2 \/ C are_weakly_separated
 proof let C be Subset of X;
  assume A1,A2 are_weakly_separated;
    then A1: A1 \ A2,A2 \ A1 are_separated by Def7;
    A2: (A1 \/ C) \ (A2 \/ C) = (A1 \ (A2 \/ C)) \/ (C \ (A2 \/ C)) by XBOOLE_1
:42
                           .= (A1 \ (A2 \/ C)) \/ {} by XBOOLE_1:46
                           .= (A1 \ A2) /\ (A1 \ C) by XBOOLE_1:53;
       (A2 \/ C) \ (A1 \/ C) = (A2 \ (A1 \/ C)) \/ (C \ (A1 \/ C)) by XBOOLE_1:
42
                           .= (A2 \ (A1 \/ C)) \/ {} by XBOOLE_1:46
                           .= (A2 \ A1) /\ (A2 \ C) by XBOOLE_1:53;
    then (A1 \/ C) \ (A2 \/ C) c= A1 \ A2 & (A2 \/ C) \ (A1 \/ C) c= A2 \ A1
                                                           by A2,XBOOLE_1:17;
    then (A1 \/ C) \ (A2 \/ C),(A2 \/ C) \ (A1 \/ C) are_separated
                                                        by A1,CONNSP_1:8;
    hence thesis by Def7;
 end;

theorem Th56:
 for B1, B2 being Subset of X st B1 c= A2 & B2 c= A1 holds
  A1,A2 are_weakly_separated implies
   A1 \/ B1,A2 \/ B2 are_weakly_separated
 proof let B1, B2 be Subset of X such that
 A1: B1 c= A2 & B2 c= A1;
   assume A1,A2 are_weakly_separated;
     then A2: A1 \ A2,A2 \ A1 are_separated by Def7;
     A3: A2 c= A2 \/ B2 & A1 c= A1 \/ B1 by XBOOLE_1:7;
    then B1 c= A2 \/ B2 & B2 c= A1 \/ B1 by A1,XBOOLE_1:1;
    then A4: B1 \ (A2 \/ B2) = {} & B2 \ (A1 \/ B1) = {} by XBOOLE_1:37;
       (A1 \/ B1) \ (A2 \/ B2) = (A1 \ (A2 \/ B2)) \/ (B1 \ (A2 \/ B2)) &
     (A2 \/ B2) \ (A1 \/ B1) = (A2 \ (A1 \/ B1)) \/ (B2 \ (A1 \/
 B1)) by XBOOLE_1:42;
    then (A1 \/ B1) \ (A2 \/ B2) c= A1 \ A2 &
         (A2 \/ B2) \ (A1 \/ B1) c= A2 \ A1 by A3,A4,XBOOLE_1:34;
    then (A1 \/ B1) \ (A2 \/ B2),(A2 \/ B2) \ (A1 \/ B1) are_separated
                                                         by A2,CONNSP_1:8;
    hence thesis by Def7;
 end;

theorem Th57:
 for B being Subset of X holds
  A1,B are_weakly_separated & A2,B are_weakly_separated
    implies A1 /\ A2,B are_weakly_separated
 proof let B be Subset of X;
  thus A1,B are_weakly_separated & A2,B are_weakly_separated implies
      A1 /\ A2,B are_weakly_separated
   proof assume A1,B are_weakly_separated & A2,B are_weakly_separated;
    then A1 \ B,B \ A1 are_separated & A2 \ B,B \ A2 are_separated by Def7;
    then (A1 \ B) /\ (A2 \ B),B \ A1 are_separated &
         (A1 \ B) /\ (A2 \ B),B \ A2 are_separated by Th44;
    then (A1 \ B) /\ (A2 \ B),(B \ A1) \/ (B \ A2) are_separated by Th45;
    then (A1 /\ A2) \ B,(B \ A1) \/ (B \ A2) are_separated by Lm3;
    then (A1 /\ A2) \ B,B \ (A1 /\ A2) are_separated by XBOOLE_1:54;
    hence thesis by Def7;
   end;
 end;

theorem Th58:
 for B being Subset of X holds
  A1,B are_weakly_separated & A2,B are_weakly_separated
    implies A1 \/ A2,B are_weakly_separated
 proof let B be Subset of X;
  thus A1,B are_weakly_separated & A2,B are_weakly_separated implies
      A1 \/ A2,B are_weakly_separated
   proof assume A1,B are_weakly_separated & A2,B are_weakly_separated;
    then A1 \ B,B \ A1 are_separated & A2 \ B,B \ A2 are_separated by Def7;
    then A1 \ B,(B \ A1) /\ (B \ A2) are_separated &
         A2 \ B,(B \ A1) /\ (B \ A2) are_separated by Th44;
    then (A1 \ B) \/ (A2 \ B),(B \ A1) /\ (B \ A2) are_separated by Th45;
    then (A1 \/ A2) \ B,(B \ A1) /\ (B \ A2) are_separated by XBOOLE_1:42;
    then (A1 \/ A2) \ B,B \ (A1 \/ A2) are_separated by XBOOLE_1:53;
    hence thesis by Def7;
   end;
 end;

::First Characterization of Weakly Separated Subsets of Topological Spaces.
theorem Th59:
 A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X
 st C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
 A2 &
   the carrier of X = (C1 \/ C2) \/ C & C1 is closed & C2 is closed & C is open
 proof
   set B1 = A1 \ A2, B2 = A2 \ A1;
A1: (A1 \/ A2)` misses (A1 \/ A2) & (B1 \/ B2)` misses (B1 \/ B2)
    by PRE_TOPC:26;
  thus A1,A2 are_weakly_separated implies
   ex C1, C2, C being Subset of X st
    C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
 A2 &
     the carrier of X = (C1 \/ C2) \/ C & C1 is closed & C2 is closed &
       C is open
   proof assume A1,A2 are_weakly_separated;
    then B1,B2 are_separated by Def7;
    then consider C1, C2 being Subset of X such that
      A2: B1 c= C1 & B2 c= C2 and A3: C1 misses B2 & C2 misses B1 and
      A4: C1 is closed & C2 is closed by Th46;
    take C1,C2;
    take C = (C1 \/ C2)`;
A5:      C1 \/ C2 is closed by A4,TOPS_1:36;
        [#]X = C \/ C` by PRE_TOPC:18;
     then A6: the carrier of X = C \/ C` by PRE_TOPC:12;
        C1 /\ B2 = {} & C2 /\ B1 = {} by A3,XBOOLE_0:def 7;
     then C1 /\ A2 \ C1 /\ A1 = {} & C2 /\ A1 \ C2 /\ A2 = {} by XBOOLE_1:50;
     then A7: C1 /\ A2 c= C1 /\ A1 & C2 /\ A1 c= C2 /\ A2 by XBOOLE_1:37;
        C1 /\ (A1 \/ A2) = C1 /\ A1 \/ C1 /\ A2 & C2 /\ (A1 \/ A2) = C2 /\ A1
\/
       C2 /\ A2 by XBOOLE_1:23;
     then A8:
 C1 /\ (A1 \/ A2) = C1 /\ A1 & C2 /\ (A1 \/ A2) = C2 /\ A2 by A7,XBOOLE_1:12;
        B1 \/ B2 c= C1 \/ C2 by A2,XBOOLE_1:13;
     then C c= (B1 \/ B2)`by PRE_TOPC:19;
     then C c= (A1 \+\ A2)` by XBOOLE_0:def 6;
     then C c= ((A1 \/ A2) \ A1 /\ A2)` by XBOOLE_1:101;
     then C c= (A1 \/ A2)` \/ (A1 /\ A2) by SUBSET_1:33;
     then C /\ (A1 \/ A2) c= ((A1 \/ A2)` \/ (A1 /\ A2)) /\ (A1 \/
 A2) by XBOOLE_1:26;
     then C /\ (A1 \/ A2) c= (A1 \/ A2)` /\ (A1 \/ A2) \/ (A1 /\ A2) /\ (A1 \/
      A2) by XBOOLE_1:23;
     then C /\ (A1 \/ A2) c= {}X \/ (A1 /\ A2) /\ (A1 \/ A2)
       by A1,XBOOLE_0:def 7;
     then C /\ (A1 \/ A2) c= (A1 /\ A2) /\ (A1 \/ A2) &
          (A1 /\ A2) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:17;
    hence thesis by A4,A5,A6,A8,TOPS_1:29,XBOOLE_1:1,17;
   end;
  given C1, C2, C being Subset of X such that A9:
    C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
 A2 and
     A10: the carrier of X = (C1 \/ C2) \/ C and
     A11: C1 is closed & C2 is closed & C is open;
     ex C1 being Subset of X, C2 being Subset of X st B1 c= C1 & B2 c= C2 &
    C1 /\ C2 misses B1 \/ B2 & C1 is closed & C2 is closed
    proof
     take C1,C2;
        A1 /\ A2 c= A1 & A1 /\ A2 c= A2 by XBOOLE_1:17;
     then C /\ (A1 \/ A2) c= A1 & C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:1;
     then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 &
          C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:8;
     then (C \/ C1) /\ (A1 \/ A2) c= A1 & (C2 \/ C) /\ (A1 \/ A2) c= A2 &
           A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7,23;
     then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) &
           B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by XBOOLE_1:35;
     then A12: B2 c= (A1 \/ A2) \ (C \/ C1) &
               B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
        A1 \/ A2 c= [#]X & [#]X = the carrier of X by PRE_TOPC:12,14;
     then A1 \/ A2 c= (C \/ C1) \/ C2 & A1 \/ A2 c= (C2 \/ C) \/
 C1 by A10,XBOOLE_1:4;
     then A13:
      (A1 \/ A2) \ (C \/ C1) c= C2 & (A1 \/ A2) \ (C2 \/ C) c= C1 by XBOOLE_1:
43;
        (C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2)) c= A1 /\ A2 by A9,XBOOLE_1:27
;
     then (C1 /\ ((A1 \/ A2) /\ C2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
     then ((C1 /\ C2) /\ (A1 \/ A2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
     then (C1 /\ C2) /\ ((A1 \/ A2) /\ (A1 \/ A2)) c= A1 /\ A2 by XBOOLE_1:16;
     then ((C1 /\ C2) /\ (A1 \/ A2)) \ (A1 /\ A2) = {} by XBOOLE_1:37;
     then (C1 /\ C2) /\ ((A1 \/ A2) \ (A1 /\ A2)) = {} by XBOOLE_1:49;
     then (C1 /\ C2) /\ (B1 \/ B2) = {} by XBOOLE_1:55;
     hence thesis by A11,A12,A13,XBOOLE_0:def 7,XBOOLE_1:1;
    end;
   then B1,B2 are_separated by Th47;
  hence A1,A2 are_weakly_separated by Def7;
 end;

reserve X for non empty TopSpace, A1, A2 for Subset of X;

theorem Th60:
 A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies
  ex C1, C2 being non empty Subset of X st
   C1 is closed & C2 is closed & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/
 A2) c= A2 &
    (A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
     C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/
 C)
 proof assume A1: A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
   set B1 = A1 \ A2, B2 = A2 \ A1;
  consider C1, C2, C being Subset of X such that
   A2: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 &
         C /\ (A1 \/ A2) c= A1 /\ A2 and
   A3: the carrier of X = (C1 \/ C2) \/ C and
   A4: C1 is closed & C2 is closed & C is open by A1,Th59;
      A1 /\ A2 c= A1 & A1 /\ A2 c= A2 by XBOOLE_1:17;
   then C /\ (A1 \/ A2) c= A1 & C /\ (A1 \/ A2) c= A2 by A2,XBOOLE_1:1;
   then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 &
        C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A2,XBOOLE_1:8;
   then (C \/ C1) /\ (A1 \/ A2) c= A1 & (C2 \/ C) /\ (A1 \/ A2) c= A2 &
         A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7,23;
   then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) &
         B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by XBOOLE_1:35;
   then A5: B2 c= (A1 \/ A2) \ (C \/ C1) &
             B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
      A1 \/ A2 c= [#]X & [#]X = the carrier of X by PRE_TOPC:12,14;
   then A1 \/ A2 c= (C \/ C1) \/ C2 & A1 \/ A2 c= (C2 \/ C) \/
 C1 by A3,XBOOLE_1:4;
   then (A1 \/ A2) \ (C \/ C1) c= C2 & (A1 \/ A2) \ (C2 \/
 C) c= C1 by XBOOLE_1:43;
   then A6:
 B2 c= C2 & B1 c= C1 & B1 <> {} & B2 <> {} by A1,A5,XBOOLE_1:1,37;
   then reconsider D1 = C1 as non empty Subset of X by XBOOLE_1:3;
   reconsider D2 = C2 as non empty Subset of X by A6,XBOOLE_1:3;
  take D1,D2;
    now assume A7: not A1 \/ A2 c= C1 \/ C2;
   thus ex C being non empty Subset of X st
        the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\
 A2 & C is open
    proof
      reconsider C0 = C as non empty Subset of X by A3,A7;
     take C0;
     thus thesis by A2,A3,A4;
    end;
  end;
  hence thesis by A2,A4;
 end;

theorem Th61:
 A1 \/ A2 = the carrier of X implies
  (A1,A2 are_weakly_separated iff
   ex C1, C2, C being Subset of X st
    A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
     C1 is closed & C2 is closed & C is open)
 proof assume A1: A1 \/ A2 = the carrier of X;
   then A2:  [#]X = A1 \/ A2 by PRE_TOPC:12;
  thus A1,A2 are_weakly_separated implies
    ex C1, C2, C being Subset of X st
    A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
     C1 is closed & C2 is closed & C is open
   proof assume A1,A2 are_weakly_separated;
    then consider C1, C2, C being Subset of X such that
    A3: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 &
          C /\ (A1 \/ A2) c= A1 /\ A2 and
    A4: the carrier of X = (C1 \/ C2) \/ C and
    A5: C1 is closed & C2 is closed & C is open by Th59;
    take C1,C2,C;
    thus thesis by A1,A2,A3,A4,A5,PRE_TOPC:15;
   end;
  given C1, C2, C being Subset of X such that
    A6: A1 \/ A2 = (C1 \/ C2) \/ C and A7: C1 c= A1 & C2 c= A2 & C c= A1 /\
 A2 and
    A8: C1 is closed & C2 is closed & C is open;
     ex C1, C2, C being Subset of X st
    C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
 A2 &
     the carrier of X = (C1 \/ C2) \/
 C & C1 is closed & C2 is closed & C is open
    proof
     take C1,C2,C;
     thus thesis by A1,A2,A6,A7,A8,PRE_TOPC:15;
    end;
   hence A1,A2 are_weakly_separated by Th59;
 end;

theorem Th62:
 A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated &
  not A1 c= A2 & not A2 c= A1 implies
   ex C1, C2 being non empty Subset of X st
    C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 &
     (A1 \/ A2 = C1 \/ C2 or ex C being non empty Subset of X st
       A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open)
 proof assume A1: A1 \/ A2 = the carrier of X;
  assume A2: A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
   A3: [#]X = A1 \/ A2 by A1,PRE_TOPC:12;
  consider C1, C2 being non empty Subset of X such that
   A4: C1 is closed & C2 is closed and
   A5: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 and
   A6: A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
       C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2)
\/ C by A2,Th60;
  take C1,C2;
     now assume not A1 \/ A2 = C1 \/ C2;
    then consider C being non empty Subset of X such that
     A7: C is open and
     A8: C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C
                                           by A1,A6,XBOOLE_0:def 10;
    thus ex C being non empty Subset of X st
          A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open
          proof
           take C;
           thus thesis by A1,A3,A7,A8,PRE_TOPC:15;
          end;
   end;
  hence thesis by A3,A4,A5,PRE_TOPC:15;
 end;

::Second Characterization of Weakly Separated Subsets of Topological Spaces.
theorem Th63:
 A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X
  st C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
 A2 &
   the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed
 proof
   set B1 = A1 \ A2, B2 = A2 \ A1;
A1: (A1 \/ A2)` misses (A1 \/ A2) & (B1 \/ B2)` misses (B1 \/ B2)
    by PRE_TOPC:26;
  thus A1,A2 are_weakly_separated implies
   ex C1, C2, C being Subset of X st
    C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
 A2 &
     the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed
   proof assume A1,A2 are_weakly_separated;
     then B1,B2 are_separated by Def7;
     then consider C1, C2 being Subset of X such that
      A2: B1 c= C1 & B2 c= C2 and A3: C1 misses B2 & C2 misses B1 and
      A4: C1 is open & C2 is open by Th48;
    take C1,C2;
    take C = (C1 \/ C2)`;
A5:      C1 \/ C2 is open by A4,TOPS_1:37;

        [#]X = C` \/ C by PRE_TOPC:18;
     then A6: the carrier of X = C` \/ C by PRE_TOPC:12;
        C1 /\ B2 = {} & C2 /\ B1 = {} by A3,XBOOLE_0:def 7;
     then C1 /\ A2 \ C1 /\ A1 = {} & C2 /\ A1 \ C2 /\ A2 = {} by XBOOLE_1:50;
     then A7: C1 /\ A2 c= C1 /\ A1 & C2 /\ A1 c= C2 /\ A2 by XBOOLE_1:37;
        C1 /\ (A1 \/ A2) = C1 /\ A1 \/ C1 /\ A2 & C2 /\ (A1 \/ A2) = C2 /\ A1
\/
 C2 /\ A2
                                                                  by XBOOLE_1:
23;
     then A8:
 C1 /\ (A1 \/ A2) = C1 /\ A1 & C2 /\ (A1 \/ A2) = C2 /\ A2 by A7,XBOOLE_1:12;
        B1 \/ B2 c= C1 \/ C2 by A2,XBOOLE_1:13;
     then C c= (B1 \/ B2)`by PRE_TOPC:19;
     then C c= (A1 \+\ A2)` by XBOOLE_0:def 6;
     then C c= ((A1 \/ A2) \ A1 /\ A2)` by XBOOLE_1:101;
     then C c= (A1 \/ A2)` \/ (A1 /\ A2) by SUBSET_1:33;
     then C /\ (A1 \/ A2) c= ((A1 \/ A2)` \/ (A1 /\ A2)) /\ (A1 \/
 A2) by XBOOLE_1:26;
     then C /\ (A1 \/ A2) c= (A1 \/ A2)` /\ (A1 \/ A2) \/ (A1 /\ A2) /\ (A1 \/
 A2) by XBOOLE_1:23;
     then C /\ (A1 \/ A2) c= {}X \/ (A1 /\ A2) /\ (A1 \/ A2)
       by A1,XBOOLE_0:def 7;
     then C /\ (A1 \/ A2) c= (A1 /\ A2) /\ (A1 \/ A2) &
          (A1 /\ A2) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:17;
    hence thesis by A4,A5,A6,A8,TOPS_1:30,XBOOLE_1:1,17;
   end;
  given C1, C2, C being Subset of X such that A9:
    C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
 A2 and
   A10: the carrier of X = (C1 \/ C2) \/ C and
   A11: C1 is open & C2 is open & C is closed;
     ex C1, C2 being Subset of X st B1 c= C1 & B2 c= C2 &
    C1 /\ C2 misses B1 \/ B2 & C1 is open & C2 is open
    proof
     take C1,C2;
        A1 /\ A2 c= A1 & A1 /\ A2 c= A2 by XBOOLE_1:17;
     then C /\ (A1 \/ A2) c= A1 & C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:1;
     then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 &
          C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:8;
     then (C \/ C1) /\ (A1 \/ A2) c= A1 & (C2 \/ C) /\ (A1 \/ A2) c= A2 &
           A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7,23;
     then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) &
           B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by XBOOLE_1:35;
     then A12: B2 c= (A1 \/ A2) \ (C \/ C1) &
               B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
        A1 \/ A2 c= [#]X & [#]X = the carrier of X by PRE_TOPC:12,14;
     then A1 \/ A2 c= (C \/ C1) \/ C2 & A1 \/ A2 c= (C2 \/ C) \/
 C1 by A10,XBOOLE_1:4;
     then A13:
         (A1 \/ A2) \ (C \/ C1) c= C2 & (A1 \/ A2) \ (C2 \/
 C) c= C1 by XBOOLE_1:43;
        (C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2)) c= A1 /\ A2 by A9,XBOOLE_1:27
;
     then (C1 /\ ((A1 \/ A2) /\ C2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
     then ((C1 /\ C2) /\ (A1 \/ A2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
     then (C1 /\ C2) /\ ((A1 \/ A2) /\ (A1 \/ A2)) c= A1 /\ A2 by XBOOLE_1:16;
     then ((C1 /\ C2) /\ (A1 \/ A2)) \ (A1 /\ A2) = {} by XBOOLE_1:37;
     then (C1 /\ C2) /\ ((A1 \/ A2) \ (A1 /\ A2)) = {} by XBOOLE_1:49;
     then (C1 /\ C2) /\ (B1 \/ B2) = {} by XBOOLE_1:55;
     hence thesis by A11,A12,A13,XBOOLE_0:def 7,XBOOLE_1:1;
    end;
   then B1,B2 are_separated by Th49;
  hence A1,A2 are_weakly_separated by Def7;
 end;

theorem Th64:
 A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1 implies
  ex C1, C2 being non empty Subset of X st
   C1 is open & C2 is open & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 &
    (A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X
     st C is closed &
     C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C)
 proof assume A1: A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
   set B1 = A1 \ A2, B2 = A2 \ A1;
  consider C1, C2, C being Subset of X such that
 A2: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
 A2 and
   A3: the carrier of X = (C1 \/ C2) \/ C and
   A4: C1 is open & C2 is open & C is closed by A1,Th63;
      A1 /\ A2 c= A1 & A1 /\ A2 c= A2 by XBOOLE_1:17;
   then C /\ (A1 \/ A2) c= A1 & C /\ (A1 \/ A2) c= A2 by A2,XBOOLE_1:1;
   then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 &
        C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A2,XBOOLE_1:8;
   then (C \/ C1) /\ (A1 \/ A2) c= A1 & (C2 \/ C) /\ (A1 \/ A2) c= A2 &
         A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7,23;
   then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) &
         B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by XBOOLE_1:35;
   then A5: B2 c= (A1 \/ A2) \ (C \/ C1) &
             B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
      A1 \/ A2 c= [#]X & [#]X = the carrier of X by PRE_TOPC:12,14;
   then A1 \/ A2 c= (C \/ C1) \/ C2 & A1 \/ A2 c= (C2 \/ C) \/
 C1 by A3,XBOOLE_1:4;
   then (A1 \/ A2) \ (C \/ C1) c= C2 & (A1 \/ A2) \ (C2 \/
 C) c= C1 by XBOOLE_1:43;
   then A6:
 B2 c= C2 & B1 c= C1 & B1 <> {} & B2 <> {} by A1,A5,XBOOLE_1:1,37;
   then reconsider D1 = C1 as non empty Subset of X by XBOOLE_1:3;
   reconsider D2 = C2 as non empty Subset of X by A6,XBOOLE_1:3;
  take D1,D2;
    now assume A7: not A1 \/ A2 c= C1 \/ C2;
   thus ex C being non empty Subset of X st
      the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\
 A2 & C is closed
    proof
      reconsider C0 = C as non empty Subset of X by A3,A7;
     take C0;
     thus thesis by A2,A3,A4;
    end;
  end;
  hence thesis by A2,A4;
 end;

theorem Th65:
 A1 \/ A2 = the carrier of X implies
  (A1,A2 are_weakly_separated iff ex C1, C2, C being Subset of X st
    A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
     C1 is open & C2 is open & C is closed)
 proof assume A1: A1 \/ A2 = the carrier of X;
     X is SubSpace of X by Th2;
  then reconsider D = the carrier of X as Subset of X by Th1;
    A2: D = [#]X by PRE_TOPC:12;
  thus A1,A2 are_weakly_separated implies
  ex C1, C2, C being Subset of X st
    A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
     C1 is open & C2 is open & C is closed
   proof assume A1,A2 are_weakly_separated;
    then consider C1, C2, C being Subset of X such that
    A3: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 &
          C /\ (A1 \/ A2) c= A1 /\ A2 and
    A4: the carrier of X = (C1 \/ C2) \/ C and
    A5: C1 is open & C2 is open & C is closed by Th63;
    take C1,C2,C;
    thus thesis by A1,A2,A3,A4,A5,PRE_TOPC:15;
   end;
  given C1, C2, C being Subset of X such that
   A6: A1 \/ A2 = (C1 \/ C2) \/ C and A7: C1 c= A1 & C2 c= A2 & C c= A1 /\
 A2 and
   A8: C1 is open & C2 is open & C is closed;
     ex C1, C2, C being Subset of X st
    C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 & C /\ (A1 \/ A2) c= A1 /\
 A2 &
     the carrier of X = (C1 \/ C2) \/ C & C1 is open & C2 is open & C is closed
    proof
     take C1,C2,C;
     thus thesis by A1,A2,A6,A7,A8,PRE_TOPC:15;
    end;
   hence A1,A2 are_weakly_separated by Th63;
 end;

theorem Th66:
 A1 \/ A2 = the carrier of X & A1,A2 are_weakly_separated &
  not A1 c= A2 & not A2 c= A1 implies
   ex C1, C2 being non empty Subset of X st
    C1 is open & C2 is open & C1 c= A1 & C2 c= A2 &
     (A1 \/ A2 = C1 \/ C2 or ex C being non empty Subset of X st
      A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed)
 proof assume A1: A1 \/ A2 = the carrier of X;
  assume A2: A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
   A3: [#]X = A1 \/ A2 by A1,PRE_TOPC:12;
  consider C1, C2 being non empty Subset of X such that
   A4: C1 is open & C2 is open and
   A5: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 and
   A6: A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
     C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2)
\/ C
                                                          by A2,Th64;
  take C1,C2;
     now assume not A1 \/ A2 = C1 \/ C2;
    then consider C being non empty Subset of X such that
     A7: C is closed and
     A8: C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C
                                                 by A1,A6,XBOOLE_0:def 10;
    thus ex C being non empty Subset of X st
          A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed
          proof
           take C;
           thus thesis by A1,A3,A7,A8,PRE_TOPC:15;
          end;
   end;
  hence thesis by A3,A4,A5,PRE_TOPC:15;
 end;

::A Characterization of Separated Subsets by means of Weakly Separated ones.
theorem Th67:
 A1,A2 are_separated iff ex B1, B2 being Subset of X st
  B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2
 proof
  thus A1,A2 are_separated implies
  ex B1, B2 being Subset of X st
    B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2
   proof assume A1,A2 are_separated;
    then consider B1, B2 being Subset of X such that
     A1: A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 and
     A2: B1 is open & B2 is open by Th49;
    take B1,B2;
    thus thesis by A1,A2,Th54;
   end;
  given B1, B2 being Subset of X such that
     A3: B1,B2 are_weakly_separated and
     A4: A1 c= B1 & A2 c= B2 and
     A5: B1 /\ B2 misses A1 \/ A2;
      A1 /\ B2 c= A1 & A1 /\ B2 c= B1 /\ B2 & B1 /\ A2 c= A2 & B1 /\ A2 c= B1
/\
 B2
                                                            by A4,XBOOLE_1:17,
26;
   then A6: A1 /\ B2 c= (B1 /\ B2) /\ A1 & B1 /\ A2 c= (B1 /\ B2) /\
 A2 by XBOOLE_1:19;
       A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7;
   then B1 /\ B2 misses A1 & B1 /\ B2 misses A2 by A5,XBOOLE_1:63;
   then (B1 /\ B2) /\ A1 = {} & (B1 /\ B2) /\ A2 = {} by XBOOLE_0:def 7;
   then A7: A1 /\ B2 = {} & B1 /\ A2 = {} by A6,XBOOLE_1:3;
      A1 \ B2 c= B1 \ B2 & A2 \ B1 c= B2 \ B1 by A4,XBOOLE_1:33;
   then A8: A1 \ A1 /\ B2 c= B1 \ B2 & A2 \ B1 /\ A2 c= B2 \ B1 by XBOOLE_1:47;
      B1 \ B2,B2 \ B1 are_separated by A3,Def7;
  hence A1,A2 are_separated by A7,A8,CONNSP_1:8;
 end;


begin
::4. Separated and Weakly Separated Subspaces of Topological Spaces.
reserve X for non empty TopSpace;

definition let X be TopStruct; let X1, X2 be SubSpace of X;
   pred X1,X2 are_separated means
:Def8: for A1, A2 being Subset of X st
  A1 = the carrier of X1 & A2 = the carrier of X2 holds
   A1,A2 are_separated;
 symmetry;
 antonym X1,X2 are_not_separated;
end;

reserve X1, X2 for non empty SubSpace of X;

::Properties of Separated Subspaces of Topological Spaces.
theorem
   X1,X2 are_separated implies X1 misses X2
 proof
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  assume X1,X2 are_separated;
   then A1,A2 are_separated by Def8;
   then A1 misses A2 by Th37;
   hence thesis by Def3;
 end;

canceled;

theorem
   for X1, X2 being closed non empty SubSpace of X holds
  X1 misses X2 iff X1,X2 are_separated
 proof let X1, X2 be closed non empty SubSpace of X;
     the carrier of X1 is Subset of X by Th1;
   then reconsider A1 = the carrier of X1 as Subset of X;
     the carrier of X2 is Subset of X by Th1;
   then reconsider A2 = the carrier of X2 as Subset of X;
    A1: A1 is closed & A2 is closed by Th11;
  thus X1 misses X2 implies X1,X2 are_separated
   proof assume X1 misses X2;
    then A1 misses A2 by Def3;
     then for A1, A2 be Subset of X holds
 A1 = the carrier of X1 & A2 = the carrier of X2 implies A1,A2 are_separated
 by A1,Th38;
    hence thesis by Def8;
   end;
  assume X1,X2 are_separated;
   then A1,A2 are_separated by Def8;
   then A1 misses A2 by CONNSP_1:2;
  hence X1 misses X2 by Def3;
 end;

theorem
   X = X1 union X2 & X1,X2 are_separated implies
  X1 is closed SubSpace of X
 proof assume
A1:  X = X1 union X2;
     the carrier of X1 is Subset of X by Th1;
   then reconsider A1 = the carrier of X1 as Subset of X;
     the carrier of X2 is Subset of X by Th1;
   then reconsider A2 = the carrier of X2 as Subset of X;
       A1 \/ A2 = the carrier of X by A1,Def2;
    then A2: A1 \/ A2 = [#]X by PRE_TOPC:12;
   assume X1,X2 are_separated;
    then A1,A2 are_separated by Def8;
    then A1 is closed & A2 is closed by A2,CONNSP_1:5;
   hence thesis by Th11;
 end;

theorem
   X1 union X2 is closed SubSpace of X & X1,X2 are_separated implies
  X1 is closed SubSpace of X
 proof
     the carrier of X1 is Subset of X by Th1;
   then reconsider A1 = the carrier of X1 as Subset of X;
     the carrier of X2 is Subset of X by Th1;
   then reconsider A2 = the carrier of X2 as Subset of X;
    A1: A1 \/ A2 = the carrier of X1 union X2 by Def2;
  assume X1 union X2 is closed SubSpace of X;
  then A2: A1 \/ A2 is closed by A1,Th11;
  assume X1,X2 are_separated;
  then A1,A2 are_separated by Def8;
  then A1 is closed & A2 is closed by A2,Th39;
  hence thesis by Th11;
 end;

theorem
   for X1, X2 being open non empty SubSpace of X holds
  X1 misses X2 iff X1,X2 are_separated
 proof let X1, X2 be open non empty SubSpace of X;
     the carrier of X1 is Subset of X by Th1;
   then reconsider A1 = the carrier of X1 as Subset of X;
     the carrier of X2 is Subset of X by Th1;
   then reconsider A2 = the carrier of X2 as Subset of X;
    A1: A1 is open & A2 is open by Th16;
  thus X1 misses X2 implies X1,X2 are_separated
   proof
    assume X1 misses X2;
    then A1 misses A2 by Def3;
     then for A1, A2 be Subset of X holds
 A1 = the carrier of X1 & A2 = the carrier of X2 implies A1,A2 are_separated
 by A1,Th41;
    hence thesis by Def8;
   end;
  assume X1,X2 are_separated;
   then A1,A2 are_separated by Def8;
   then A1 misses A2 by CONNSP_1:2;
  hence X1 misses X2 by Def3;
 end;

theorem
   X = X1 union X2 & X1,X2 are_separated implies
  X1 is open SubSpace of X
 proof
   assume A1: X = X1 union X2;
      the carrier of X1 is Subset of X by Th1;
    then reconsider A1 = the carrier of X1 as Subset of X;
      the carrier of X2 is Subset of X by Th1;
    then reconsider A2 = the carrier of X2 as Subset of X;
       A1 \/ A2 = the carrier of X by A1,Def2;
    then A2: A1 \/ A2 = [#]X by PRE_TOPC:12;
   assume X1,X2 are_separated;
    then A1,A2 are_separated by Def8;
    then A1 is open & A2 is open by A2,CONNSP_1:5;
   hence thesis by Th16;
 end;

theorem
   X1 union X2 is open SubSpace of X & X1,X2 are_separated implies
  X1 is open SubSpace of X
 proof
     the carrier of X1 is Subset of X by Th1;
   then reconsider A1 = the carrier of X1 as Subset of X;
     the carrier of X2 is Subset of X by Th1;
   then reconsider A2 = the carrier of X2 as Subset of X;
    A1: A1 \/ A2 = the carrier of X1 union X2 by Def2;
  assume X1 union X2 is open SubSpace of X;
  then A2: A1 \/ A2 is open by A1,Th16;
  assume X1,X2 are_separated;
  then A1,A2 are_separated by Def8;
  then A1 is open & A2 is open by A2,Th42;
  hence thesis by Th16;
 end;

::Restriction Theorems for Separated Subspaces.
theorem
   for Y, X1, X2 being non empty SubSpace of X st X1 meets Y & X2 meets Y holds
  X1,X2 are_separated implies
   X1 meet Y,X2 meet Y are_separated & Y meet X1,Y meet X2 are_separated
 proof let Y, X1, X2 be non empty SubSpace of X such that
 A1: X1 meets Y & X2 meets Y;
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
   reconsider C = the carrier of Y as Subset of X by Th1;
  assume A2: X1,X2 are_separated;
  thus A3: X1 meet Y,X2 meet Y are_separated
   proof
     A4: A1,A2 are_separated by A2,Def8;
      now let D1, D2 be Subset of X;
     assume D1 = the carrier of X1 meet Y & D2 = the carrier of X2 meet Y;
      then A1 /\ C = D1 & A2 /\ C = D2 by A1,Def5;
     hence D1,D2 are_separated by A4,Th43;
    end;
    hence thesis by Def8;
   end;
  thus Y meet X1,Y meet X2 are_separated
   proof
       X1 meet Y,Y meet X2 are_separated by A1,A3,Th29;
    hence thesis by A1,Th29;
   end;
 end;

theorem Th77:
 for Y1, Y2 being SubSpace of X st
  Y1 is SubSpace of X1 & Y2 is SubSpace of X2 holds
   X1,X2 are_separated implies Y1,Y2 are_separated
 proof let Y1, Y2 be SubSpace of X such that
    A1: Y1 is SubSpace of X1 & Y2 is SubSpace of X2;
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
  assume A2: X1,X2 are_separated;
     now let B1, B2 be Subset of X;
    assume B1 = the carrier of Y1 & B2 = the carrier of Y2;
     then A1,A2 are_separated & B1 c= A1 & B2 c= A2 by A1,A2,Def8,Th4;
     hence B1,B2 are_separated by CONNSP_1:8;
   end;
  hence Y1,Y2 are_separated by Def8;
 end;

theorem
   for Y being non empty SubSpace of X st X1 meets X2 holds
  X1,Y are_separated implies X1 meet X2,Y are_separated
 proof let Y be non empty SubSpace of X;
  assume X1 meets X2;
   then A1: X1 meet X2 is SubSpace of X1 by Th30;
     Y is SubSpace of Y by Th2;
  hence thesis by A1,Th77;
 end;

theorem
   for Y being non empty SubSpace of X holds
   X1,Y are_separated & X2,Y are_separated iff X1 union X2,Y are_separated
 proof let Y be non empty SubSpace of X;
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
   reconsider C = the carrier of Y as Subset of X by Th1;
    thus
      X1,Y are_separated & X2,Y are_separated implies X1 union X2,Y
are_separated
     proof assume X1,Y are_separated & X2,Y are_separated;
      then A1: A1,C are_separated & A2,C are_separated by Def8;
          now let D, C be Subset of X; assume
         A2: D = the carrier of X1 union X2 & C = the carrier of Y;
          then A1 \/ A2 = D by Def2;
         hence D,C are_separated by A1,A2,Th45;
        end;
      hence thesis by Def8;
     end;
      assume A3: X1 union X2,Y are_separated;
         X1 is SubSpace of X1 union X2 & X2 is SubSpace of X1 union X2
        & Y is SubSpace of Y by Th2,Th22;
       hence thesis by A3,Th77;
 end;

theorem
   X1,X2 are_separated iff ex Y1, Y2 being closed non empty SubSpace of X st
  X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1
 proof
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
  thus X1,X2 are_separated implies
    ex Y1, Y2 being closed non empty SubSpace of X st
     X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1
   proof assume X1,X2 are_separated;
     then A1,A2 are_separated by Def8;
     then consider C1, C2 being Subset of X such that
      A1: A1 c= C1 & A2 c= C2 and A2: C1 misses A2 & C2 misses A1 and
      A3: C1 is closed & C2 is closed by Th46;
      A4: C1 is non empty & C2 is non empty by A1,XBOOLE_1:3;
       then consider Y1 being strict closed non empty SubSpace of X such that
        A5: C1 = the carrier of Y1 by A3,Th15;
       consider Y2 being strict closed non empty SubSpace of X such that
        A6: C2 = the carrier of Y2 by A3,A4,Th15;
      take Y1,Y2;
     thus thesis by A1,A2,A5,A6,Def3,Th4;
   end;
  given Y1, Y2 being closed non empty SubSpace of X such that
   A7: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
   A8: Y1 misses X2 & Y2 misses X1;
     now let A1, A2 be Subset of X such that
     A9: A1 = the carrier of X1 & A2 = the carrier of X2;
      ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
     C1 misses A2 & C2 misses A1 & C1 is closed & C2 is closed
     proof
         the carrier of Y1 is Subset of X by Th1;
       then reconsider C1 = the carrier of Y1 as Subset of X;
         the carrier of Y2 is Subset of X by Th1;
       then reconsider C2 = the carrier of Y2 as Subset of X;
      take C1,C2;
      thus thesis by A7,A8,A9,Def3,Th4,Th11;
     end;
    hence A1,A2 are_separated by Th46;
   end;
  hence X1,X2 are_separated by Def8;
 end;

::First Characterization of Separated Subspaces of Topological Spaces.
theorem
   X1,X2 are_separated iff ex Y1, Y2 being closed non empty SubSpace of X st
  X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &
   (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
 proof
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
  thus X1,X2 are_separated implies
    ex Y1, Y2 being closed non empty SubSpace of X st
      X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &
    (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
   proof assume X1,X2 are_separated;
     then A1,A2 are_separated by Def8;
     then consider C1, C2 being Subset of X such that
      A1: A1 c= C1 & A2 c= C2 and A2: C1 /\ C2 misses A1 \/ A2 and
      A3: C1 is closed & C2 is closed by Th47;
      A4: C1 is non empty & C2 is non empty by A1,XBOOLE_1:3;
       then consider Y1 being strict closed non empty SubSpace of X such that
        A5: C1 = the carrier of Y1 by A3,Th15;
       consider Y2 being strict closed non empty SubSpace of X such that
        A6: C2 = the carrier of Y2 by A3,A4,Th15;
      take Y1,Y2;
        now assume not Y1 misses Y2;
       then A7: the carrier of Y1 meet Y2 = C1 /\ C2 by A5,A6,Def5;
          the carrier of X1 union X2 = A1 \/ A2 by Def2;
       hence Y1 meet Y2 misses X1 union X2 by A2,A7,Def3;
      end;
     hence thesis by A1,A5,A6,Th4;
   end;
  given Y1, Y2 being closed non empty SubSpace of X such that
   A8: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
   A9: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
     now let A1, A2 be Subset of X such that
     A10: A1 = the carrier of X1 & A2 = the carrier of X2;
      ex C1 being Subset of X, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
     C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed
     proof
         the carrier of Y1 is Subset of X by Th1;
       then reconsider C1 = the carrier of Y1 as Subset of X;
         the carrier of Y2 is Subset of X by Th1;
       then reconsider C2 = the carrier of Y2 as Subset of X;
      take C1,C2;
         now per cases;
        suppose Y1 misses Y2;
         then C1 misses C2 by Def3;
         then C1 /\ C2 = {} by XBOOLE_0:def 7;
         hence C1 /\ C2 misses A1 \/ A2 by XBOOLE_1:65;
        suppose A11: not Y1 misses Y2;
         then the carrier of Y1 meet Y2 = C1 /\ C2 &
                  the carrier of X1 union X2 = A1 \/ A2 by A10,Def2,Def5;
         hence C1 /\ C2 misses A1 \/ A2 by A9,A11,Def3;
       end;
      hence thesis by A8,A10,Th4,Th11;
     end;
    hence A1,A2 are_separated by Th47;
   end;
  hence X1,X2 are_separated by Def8;
 end;

theorem
   X1,X2 are_separated iff ex Y1, Y2 being open non empty SubSpace of X st
  X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1
 proof
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
  thus X1,X2 are_separated implies
   ex Y1,Y2 being open non empty SubSpace of X st
    X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1
   proof assume X1,X2 are_separated;
     then A1,A2 are_separated by Def8;
     then consider C1 being Subset of X,
                   C2 being Subset of X such that
      A1: A1 c= C1 & A2 c= C2 and A2: C1 misses A2 & C2 misses A1 and
      A3: C1 is open & C2 is open by Th48;
      A4: C1 is non empty & C2 is non empty by A1,XBOOLE_1:3;
       then consider Y1 being strict open non empty SubSpace of X such that
        A5: C1 = the carrier of Y1 by A3,Th20;
       consider Y2 being strict open non empty SubSpace of X such that
        A6: C2 = the carrier of Y2 by A3,A4,Th20;
      take Y1,Y2;
     thus thesis by A1,A2,A5,A6,Def3,Th4;
   end;
  given Y1, Y2 being open non empty SubSpace of X such that
   A7: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
   A8: Y1 misses X2 & Y2 misses X1;
     now let A1, A2 be Subset of X such that
     A9: A1 = the carrier of X1 & A2 = the carrier of X2;
      ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
     C1 misses A2 & C2 misses A1 & C1 is open & C2 is open
     proof
         the carrier of Y1 is Subset of X by Th1;
       then reconsider C1 = the carrier of Y1 as Subset of X;
         the carrier of Y2 is Subset of X by Th1;
       then reconsider C2 = the carrier of Y2 as Subset of X;
      take C1,C2;
      thus thesis by A7,A8,A9,Def3,Th4,Th16;
     end;
    hence A1,A2 are_separated by Th48;
   end;
  hence X1,X2 are_separated by Def8;
 end;

::Second Characterization of Separated Subspaces of Topological Spaces.
theorem Th83:
 X1,X2 are_separated iff ex Y1, Y2 being open non empty SubSpace of X st
  X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &
   (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
 proof
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
  thus X1,X2 are_separated implies
   ex Y1, Y2 being open non empty SubSpace of X st
    X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &
     (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
   proof assume X1,X2 are_separated;
     then A1,A2 are_separated by Def8;
     then consider C1, C2 being Subset of X such that
      A1: A1 c= C1 & A2 c= C2 and A2: C1 /\ C2 misses A1 \/ A2 and
      A3: C1 is open & C2 is open by Th49;
      A4: C1 is non empty & C2 is non empty by A1,XBOOLE_1:3;
       then consider Y1 being strict open non empty SubSpace of X such that
        A5: C1 = the carrier of Y1 by A3,Th20;
       consider Y2 being strict open non empty SubSpace of X such that
        A6: C2 = the carrier of Y2 by A3,A4,Th20;
      take Y1,Y2;
        now assume not Y1 misses Y2;
       then A7: the carrier of Y1 meet Y2 = C1 /\ C2 by A5,A6,Def5;
          the carrier of X1 union X2 = A1 \/ A2 by Def2;
       hence Y1 meet Y2 misses X1 union X2 by A2,A7,Def3;
      end;
     hence thesis by A1,A5,A6,Th4;
   end;
  given Y1, Y2 being open non empty SubSpace of X such that
   A8: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
   A9: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
     now let A1, A2 be Subset of X such that
     A10: A1 = the carrier of X1 & A2 = the carrier of X2;
      ex C1, C2 being Subset of X st A1 c= C1 & A2 c= C2 &
     C1 /\ C2 misses A1 \/ A2 & C1 is open & C2 is open
     proof
         the carrier of Y1 is Subset of X by Th1;
       then reconsider C1 = the carrier of Y1 as Subset of X;
         the carrier of Y2 is Subset of X by Th1;
       then reconsider C2 = the carrier of Y2 as Subset of X;
      take C1,C2;
         now per cases;
        suppose Y1 misses Y2;
         then C1 misses C2 by Def3;
         then C1 /\ C2 = {} by XBOOLE_0:def 7;
         hence C1 /\ C2 misses A1 \/ A2 by XBOOLE_1:65;
        suppose A11: not Y1 misses Y2;
         then the carrier of Y1 meet Y2 = C1 /\ C2 &
                  the carrier of X1 union X2 = A1 \/ A2 by A10,Def2,Def5;
         hence C1 /\ C2 misses A1 \/ A2 by A9,A11,Def3;
       end;
      hence thesis by A8,A10,Th4,Th16;
     end;
    hence A1,A2 are_separated by Th49;
   end;
  hence X1,X2 are_separated by Def8;
 end;

definition let X be TopStruct, X1, X2 be SubSpace of X;
   pred X1,X2 are_weakly_separated means
:Def9: for A1, A2 being Subset of X st
  A1 = the carrier of X1 & A2 = the carrier of X2 holds
   A1,A2 are_weakly_separated;
 symmetry;
 antonym X1,X2 are_not_weakly_separated;
end;

reserve X1, X2 for non empty SubSpace of X;

::Properties of Weakly Separated Subspaces of Topological Spaces.
canceled;

theorem Th85:
 X1 misses X2 & X1,X2 are_weakly_separated iff X1,X2 are_separated
 proof
    reconsider A1 = the carrier of X1 as Subset of X by Th1;
    reconsider A2 = the carrier of X2 as Subset of X by Th1;
  thus X1 misses X2 & X1,X2 are_weakly_separated implies X1,X2 are_separated
   proof
    assume X1 misses X2 & X1,X2 are_weakly_separated;
    then A1 misses A2 & A1,A2 are_weakly_separated by Def3,Def9;
     then for A1, A2 be Subset of X holds
 A1 = the carrier of X1 & A2 = the carrier of X2 implies A1,A2 are_separated
 by Th51;
    hence X1,X2 are_separated by Def8;
   end;
    assume X1,X2 are_separated;
    then A1: A1,A2 are_separated by Def8;
    then A1 misses A2 & A1,A2 are_weakly_separated by Th51;
    hence X1 misses X2 by Def3;
       for A1, A2 be Subset of X holds
 A1 = the carrier of X1 & A2 = the carrier of X2 implies
 A1,A2 are_weakly_separated by A1,Th51;
    hence X1,X2 are_weakly_separated by Def9;
 end;

theorem Th86:
 X1 is SubSpace of X2 implies X1,X2 are_weakly_separated
 proof assume A1: X1 is SubSpace of X2;
    now assume A2: X1 is SubSpace of X2;
        now let A1, A2 be Subset of X;
       assume A1 = the carrier of X1 & A2 = the carrier of X2;
       then A1 c= A2 by A2,Th4;
       hence A1,A2 are_weakly_separated by Th52;
      end;
      hence thesis by Def9;
     end;
  hence thesis by A1;
 end;

theorem Th87:
 for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated
 proof
  let X1, X2 be closed SubSpace of X;
     now let A1, A2 be Subset of X;
    reconsider B1 = A1, B2 = A2 as Subset of X;
     assume A1 = the carrier of X1 & A2 = the carrier of X2;
     then B1 is closed & B2 is closed by Th11;
    hence A1,A2 are_weakly_separated by Th53;
   end;
  hence thesis by Def9;
 end;

theorem Th88:
 for X1, X2 being open SubSpace of X holds X1,X2 are_weakly_separated
 proof
  let X1, X2 be open SubSpace of X;
     now let A1, A2 be Subset of X;
   reconsider B1 = A1, B2 = A2 as Subset of X;
     assume A1 = the carrier of X1 & A2 = the carrier of X2;
    then B1 is open & B2 is open by Th16;
    hence A1,A2 are_weakly_separated by Th54;
   end;
  hence thesis by Def9;
 end;

::Extension Theorems for Weakly Separated Subspaces.
theorem
   for Y being non empty SubSpace of X holds
  X1,X2 are_weakly_separated implies
   X1 union Y,X2 union Y are_weakly_separated
 proof let Y be non empty SubSpace of X;
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
   reconsider C = the carrier of Y as Subset of X by Th1;
  assume X1,X2 are_weakly_separated;
   then A1: A1,A2 are_weakly_separated by Def9;
      now let D1, D2 be Subset of X;
     assume D1 = the carrier of X1 union Y & D2 = the carrier of X2 union Y;
     then A1 \/ C = D1 & A2 \/ C = D2 by Def2;
     hence D1,D2 are_weakly_separated by A1,Th55;
    end;
    hence thesis by Def9;
 end;

theorem
   for Y1, Y2 being non empty SubSpace of X st
  Y1 is SubSpace of X2 & Y2 is SubSpace of X1 holds
   X1,X2 are_weakly_separated implies
    X1 union Y1,X2 union Y2 are_weakly_separated &
     Y1 union X1,Y2 union X2 are_weakly_separated
 proof
  let Y1, Y2 be non empty SubSpace of X such that
    A1: Y1 is SubSpace of X2 & Y2 is SubSpace of X1;
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
   reconsider B1 = the carrier of Y1 as Subset of X by Th1;
   reconsider B2 = the carrier of Y2 as Subset of X by Th1;
    A2: B1 c= A2 & B2 c= A1 by A1,Th4;
  assume X1,X2 are_weakly_separated;
   then A3: A1,A2 are_weakly_separated by Def9;
  thus X1 union Y1,X2 union Y2 are_weakly_separated
   proof
      now let D1, D2 be Subset of X;
     assume D1 = the carrier of X1 union Y1 & D2 = the carrier of X2 union Y2;
     then A1 \/ B1 = D1 & A2 \/ B2 = D2 by Def2;
     hence D1,D2 are_weakly_separated by A2,A3,Th56;
    end;
    hence thesis by Def9;
   end;
  hence Y1 union X1,Y2 union X2 are_weakly_separated;
 end;

theorem
   for Y, X1, X2 being non empty SubSpace of X st X1 meets X2 holds
  (X1,Y are_weakly_separated & X2,Y are_weakly_separated
    implies X1 meet X2,Y are_weakly_separated)
 & (Y,X1 are_weakly_separated & Y,X2 are_weakly_separated
     implies Y,X1 meet X2 are_weakly_separated)
 proof let Y, X1, X2 be non empty SubSpace of X such that A1: X1 meets X2;
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
   reconsider C = the carrier of Y as Subset of X by Th1;
  thus X1,Y are_weakly_separated & X2,Y are_weakly_separated
           implies X1 meet X2,Y are_weakly_separated
   proof assume X1,Y are_weakly_separated & X2,Y are_weakly_separated;
    then A2: A1,C are_weakly_separated & A2,C are_weakly_separated by Def9;
        now let D, C be Subset of X; assume
       A3: D = the carrier of X1 meet X2 & C = the carrier of Y;
        then A1 /\ A2 = D by A1,Def5;
       hence D,C are_weakly_separated by A2,A3,Th57;
      end;
    hence thesis by Def9;
   end;
  hence Y,X1 are_weakly_separated & Y,X2 are_weakly_separated
        implies Y,X1 meet X2 are_weakly_separated;
 end;

theorem
   for Y being non empty SubSpace of X holds
   (X1,Y are_weakly_separated & X2,Y are_weakly_separated
     implies X1 union X2,Y are_weakly_separated)
  & (Y,X1 are_weakly_separated & Y,X2 are_weakly_separated
      implies Y,X1 union X2 are_weakly_separated)
 proof let Y be non empty SubSpace of X;
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
   reconsider C = the carrier of Y as Subset of X by Th1;
  thus X1,Y are_weakly_separated & X2,Y are_weakly_separated
           implies X1 union X2,Y are_weakly_separated
   proof assume X1,Y are_weakly_separated & X2,Y are_weakly_separated;
    then A1: A1,C are_weakly_separated & A2,C are_weakly_separated by Def9;
        now let D, C be Subset of X; assume
        A2: D = the carrier of X1 union X2 & C = the carrier of Y;
         then A1 \/ A2 = D by Def2;
       hence D,C are_weakly_separated by A1,A2,Th58;
      end;
     hence thesis by Def9;
   end;
  hence Y,X1 are_weakly_separated & Y,X2 are_weakly_separated
        implies Y,X1 union X2 are_weakly_separated;
 end;

::First Characterization of Weakly Separated Subspaces of Topological Spaces.
theorem
   for X being non empty TopSpace, X1,X2 being non empty SubSpace of X holds
  X1 meets X2 implies (X1,X2 are_weakly_separated iff
   (X1 is SubSpace of X2 or X2 is SubSpace of X1 or
     ex Y1, Y2 being closed non empty SubSpace of X st
        Y1 meet (X1 union X2) is SubSpace of X1 &
         Y2 meet (X1 union X2) is SubSpace of X2 &
            (X1 union X2 is SubSpace of Y1 union Y2 or
                ex Y being open non empty SubSpace of X st
                    the TopStruct of X = (Y1 union Y2) union Y &
                      Y meet (X1 union X2) is SubSpace of X1 meet X2)))
 proof let X be non empty TopSpace, X1,X2 be non empty SubSpace of X;
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
    A1: [#]X = the carrier of X by PRE_TOPC:12;
    A2: X is SubSpace of X by Th2;
  assume A3: X1 meets X2;
  A4:now assume X1,X2 are_weakly_separated;
      then A5: A1,A2 are_weakly_separated by Def9;
       now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
      then A6: not A1 c= A2 & not A2 c= A1 by Th4;
      then consider C1, C2 being non empty Subset of X such that
        A7: C1 is closed & C2 is closed and
        A8: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 and
        A9: A1 \/ A2 c= C1 \/ C2 or
            ex C being non empty Subset of X st C is open &
             C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C
                                                         by A5,Th60;
      A10:now assume C1 misses (A1 \/ A2);
       then A11: C1 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
            now per cases;
           suppose A1 \/ A2 c= C1 \/ C2;
            then A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
                        .= {} \/ (C2 /\ (A1 \/ A2)) by A11,XBOOLE_1:23
                        .= C2 /\ (A1 \/ A2);
            then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by A8,XBOOLE_1:7;
            hence contradiction by A6,XBOOLE_1:1;
           suppose not A1 \/ A2 c= C1 \/ C2;
            then consider C being non empty Subset of X
            such that
             A12: C is open & C /\ (A1 \/ A2) c= A1 /\ A2 and
             A13: the carrier of X = (C1 \/ C2) \/ C by A9;
              A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,A13,PRE_TOPC:15
                   .= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
                   .= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A11,XBOOLE_1:23
                   .= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
            then A1 \/ A2 c= A2 \/ A1 /\ A2 & A1 /\ A2 c= A2
                                          by A8,A12,XBOOLE_1:13,17;
            then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by XBOOLE_1:7,12;
            hence contradiction by A6,XBOOLE_1:1;
          end;
          hence contradiction;
         end;
      A14:now assume C2 misses (A1 \/ A2);
          then A15: C2 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
            now per cases;
           suppose A1 \/ A2 c= C1 \/ C2;
            then A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
                        .= (C1 /\ (A1 \/ A2)) \/ {} by A15,XBOOLE_1:23
                        .= C1 /\ (A1 \/ A2);
            then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by A8,XBOOLE_1:7;
            hence contradiction by A6,XBOOLE_1:1;
           suppose not A1 \/ A2 c= C1 \/ C2;
            then consider C being non empty Subset of X such that
             A16: C is open & C /\ (A1 \/ A2) c= A1 /\ A2 and
             A17: the carrier of X = (C1 \/ C2) \/ C by A9;
              A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A1,A17,PRE_TOPC:15
                   .= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
                   .= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A15,XBOOLE_1:23
                   .= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
            then A1 \/ A2 c= A1 \/ A1 /\ A2 & A1 /\ A2 c= A1
                                          by A8,A16,XBOOLE_1:13,17;
            then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by XBOOLE_1:7,12;
            hence contradiction by A6,XBOOLE_1:1;
          end;
          hence contradiction;
         end;
      thus ex Y1, Y2 being closed non empty SubSpace of X st
         Y1 meet (X1 union X2) is SubSpace of X1 &
          Y2 meet (X1 union X2) is SubSpace of X2 &
           (X1 union X2 is SubSpace of Y1 union Y2 or
           ex Y being open non empty SubSpace of X st
              the TopStruct of X = (Y1 union Y2) union Y &
             Y meet (X1 union X2) is SubSpace of X1 meet X2)
       proof
          consider Y1 being strict closed non empty SubSpace of X such that
            A18: C1 = the carrier of Y1 by A7,Th15;
          consider Y2 being strict closed non empty SubSpace of X such that
            A19: C2 = the carrier of Y2 by A7,Th15;
        take Y1,Y2;
         A20: the carrier of X1 union X2 = A1 \/ A2 &
              the carrier of Y1 union Y2 = C1 \/ C2 by A18,A19,Def2;
        then Y1 meets (X1 union X2) & Y2 meets (X1 union X2)
                                                by A10,A14,A18,A19,Def3;
        then A21: the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) &
             the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2)
                                                by A18,A19,A20,Def5;
          now assume A22: not X1 union X2 is SubSpace of Y1 union Y2;
         then A23: not A1 \/ A2 c= C1 \/ C2 by A20,Th4;
         consider C being non empty Subset of X such that
          A24: C is open & C /\ (A1 \/ A2) c= A1 /\ A2 &
               the carrier of X = (C1 \/ C2) \/ C by A9,A20,A22,Th4;
         thus ex Y being open non empty SubSpace of X st
               the TopStruct of X = (Y1 union Y2) union Y &
                Y meet (X1 union X2) is SubSpace of X1 meet X2
          proof
           consider Y being strict open non empty SubSpace of X such that
            A25: C = the carrier of Y by A24,Th20;
           take Y;
             A26: the carrier of X = (the carrier of Y1 union Y2) \/ C
                                                    by A18,A19,A24,Def2
                    .= the carrier of (Y1 union Y2) union Y by A25,Def2;
               now assume C misses (A1 \/ A2);
               then A27: C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
                 A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,A24,PRE_TOPC:
15
                      .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A27,XBOOLE_1:23
                      .= (C1 \/ C2) /\ (A1 \/ A2);
              hence contradiction by A23,XBOOLE_1:17;
             end;
            then Y meets (X1 union X2) by A20,A25,Def3;
           then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) &
                the carrier of X1 meet X2 = A1 /\ A2 by A3,A20,A25,Def5;
           hence thesis by A2,A24,A26,Th4,Th5;
          end;
        end;
        hence thesis by A8,A21,Th4;
       end;
     end;
     hence X1 is SubSpace of X2 or X2 is SubSpace of X1
       or ex Y1, Y2 being closed non empty SubSpace of X st
        Y1 meet (X1 union X2) is SubSpace of X1 &
         Y2 meet (X1 union X2) is SubSpace of X2 &
          (X1 union X2 is SubSpace of Y1 union Y2
           or ex Y being open non empty SubSpace of X st
              the TopStruct of X = (Y1 union Y2) union Y &
            Y meet (X1 union X2) is SubSpace of X1 meet X2);
    end;
    now assume A28:
    X1 is SubSpace of X2 or X2 is SubSpace of X1
     or ex Y1, Y2 being closed non empty SubSpace of X st
      Y1 meet (X1 union X2) is SubSpace of X1 &
       Y2 meet (X1 union X2) is SubSpace of X2 &
        (X1 union X2 is SubSpace of Y1 union Y2
         or ex Y being open non empty SubSpace of X st
            the TopStruct of X = (Y1 union Y2) union Y &
          Y meet (X1 union X2) is SubSpace of X1 meet X2);
     now assume A29: not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
    then consider Y1, Y2 being closed non empty SubSpace of X such that
       A30: Y1 meet (X1 union X2) is SubSpace of X1 &
           Y2 meet (X1 union X2) is SubSpace of X2 and
       A31: X1 union X2 is SubSpace of Y1 union Y2 or
            ex Y being open non empty SubSpace of X st
             the TopStruct of X = (Y1 union Y2) union Y &
              Y meet (X1 union X2) is SubSpace of X1 meet X2 by A28;
       the carrier of Y1 is Subset of X by Th1;
     then reconsider C1 = the carrier of Y1 as Subset of X;
       the carrier of Y2 is Subset of X by Th1;
     then reconsider C2 = the carrier of Y2 as Subset of X;
       A32: C1 is closed & C2 is closed by Th11;
      A33: the carrier of X1 union X2 = A1 \/ A2 &
           the carrier of Y1 union Y2 = C1 \/ C2 by Def2;
     A34:now assume Y1 misses (X1 union X2);
          then A35: C1 misses (A1 \/ A2) by A33,Def3;
           now per cases;
          suppose X1 union X2 is SubSpace of Y1 union Y2;
           then A1 \/ A2 c= C1 \/ C2 by A33,Th4;
           then A36: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
              .= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
                           .= {} \/ (C2 /\ (A1 \/ A2)) by A35,XBOOLE_0:def 7
                           .= C2 /\ (A1 \/ A2);
           then C2 meets (A1 \/ A2) by A33,XBOOLE_0:def 7;
           then Y2 meets (X1 union X2) by A33,Def3;
           then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2)
                                                                by A33,Def5;
           hence A1 \/ A2 c= A2 by A30,A36,Th4;
          suppose not X1 union X2 is SubSpace of Y1 union Y2;
           then consider Y being open non empty SubSpace of X such that
            A37: the TopStruct of X = (Y1 union Y2) union Y and
            A38: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A31;
           reconsider C = the carrier of Y as Subset of X
           by Th1;
             the carrier of X = (C1 \/ C2) \/ C by A33,A37,Def2;
           then A39:A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC:
15
                     .= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
                     .= (C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/
 A2)) by XBOOLE_1:23
                     .= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A35,XBOOLE_0:def 7
                     .= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
            A40: now assume C2 /\ (A1 \/ A2) <> {};
                  then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y2 meets (X1 union X2) by A33,Def3;
                  then A41: the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/
A2)
                                                                by A33,Def5;
                  then A42: C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
                      now per cases;
                     suppose C /\ (A1 \/ A2) = {};
                      hence A1 \/ A2 c= A2 by A30,A39,A41,Th4;
                     suppose C /\ (A1 \/ A2) <> {};
                      then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                      then Y meets (X1 union X2) by A33,Def3;
                      then the carrier of Y meet (X1 union X2) = C /\ (A1 \/
 A2)
                         & the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
                      then C /\ (A1 \/ A2) c= A1 /\ A2 by A38,Th4;
                      then A1 \/ A2 c= A2 \/ A1 /\ A2 & A1 /\ A2 c= A2
                                            by A39,A42,XBOOLE_1:13,17;
                      hence A1 \/ A2 c= A2 by XBOOLE_1:12;
                     end;
                  hence A1 \/ A2 c= A2;
                 end;
               now assume C /\ (A1 \/ A2) <> {};
                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y meets (X1 union X2) by A33,Def3;
                  then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
                     & the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
                  then A43: C /\ (A1 \/ A2) c= A1 /\ A2 & A1 /\ A2 c= A2
                                             by A38,Th4,XBOOLE_1:17;
                  then A44: C /\ (A1 \/ A2) c= A2 by XBOOLE_1:1;
                      now per cases;
                     suppose C2 /\ (A1 \/ A2) = {};
                      hence A1 \/ A2 c= A2 by A39,A43,XBOOLE_1:1;
                     suppose C2 /\ (A1 \/ A2) <> {};
                      then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
                      then Y2 meets (X1 union X2) by A33,Def3;
                     then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/
                      A2) by A33,Def5;
                     then C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
                      hence A1 \/ A2 c= A2 by A39,A44,XBOOLE_1:8;
                     end;
                  hence A1 \/ A2 c= A2;
                 end;
           hence A1 \/ A2 c= A2 by A33,A39,A40;
         end;
          then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by XBOOLE_1:7;
          then A1 c= A2 by XBOOLE_1:1;
         hence contradiction by A29,Th4;
        end;
          now assume not Y2 meets (X1 union X2);
          then A45: C2 misses (A1 \/ A2) by A33,Def3;
           now per cases;
          suppose X1 union X2 is SubSpace of Y1 union Y2;
           then A1 \/ A2 c= C1 \/ C2 by A33,Th4;
           then A46: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
                           .= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/
 A2)) by XBOOLE_1:23
                           .= (C1 /\ (A1 \/ A2)) \/ {} by A45,XBOOLE_0:def 7
                           .= C1 /\ (A1 \/ A2);
           then C1 meets (A1 \/ A2) by A33,XBOOLE_0:def 7;
           then Y1 meets (X1 union X2) by A33,Def3;
           then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2)
                                                                by A33,Def5;
           hence A1 \/ A2 c= A1 by A30,A46,Th4;
          suppose not X1 union X2 is SubSpace of Y1 union Y2;
           then consider Y being open non empty SubSpace of X such that
            A47: the TopStruct of X = (Y1 union Y2) union Y and
            A48: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A31;
           reconsider C = the carrier of Y as Subset of X
           by Th1;
             the carrier of X = (C1 \/ C2) \/ C by A33,A47,Def2;
           then A49:A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC:
15
                     .= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
                     .= (C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/
 A2)) by XBOOLE_1:23
                     .= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A45,XBOOLE_0:def 7
                     .= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
            A50: now assume C1 /\ (A1 \/ A2) <> {};
                  then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y1 meets (X1 union X2) by A33,Def3;
                  then A51: the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/
A2)
                                                                by A33,Def5;
                  then A52: C1 /\ (A1 \/ A2) c= A1 by A30,Th4;
                      now per cases;
                     suppose C /\ (A1 \/ A2) = {};
                      hence A1 \/ A2 c= A1 by A30,A49,A51,Th4;
                     suppose C /\ (A1 \/ A2) <> {};
                      then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                      then Y meets (X1 union X2) by A33,Def3;
                      then the carrier of Y meet (X1 union X2) = C /\ (A1 \/
 A2)
                         & the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
                      then C /\ (A1 \/ A2) c= A1 /\ A2 by A48,Th4;
                      then A1 \/ A2 c= A1 \/ A1 /\ A2 & A1 /\ A2 c= A1
                                                 by A49,A52,XBOOLE_1:13,17;
                      hence A1 \/ A2 c= A1 by XBOOLE_1:12;
                     end;
                  hence A1 \/ A2 c= A1;
                 end;
               now assume C /\ (A1 \/ A2) <> {};
                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y meets (X1 union X2) by A33,Def3;
                  then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
                     & the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
                  then A53: C /\ (A1 \/ A2) c= A1 /\ A2 & A1 /\ A2 c= A1
                                                    by A48,Th4,XBOOLE_1:17;
                  then A54: C /\ (A1 \/ A2) c= A1 by XBOOLE_1:1;
                      now per cases;
                     suppose C1 /\ (A1 \/ A2) = {};
                      hence A1 \/ A2 c= A1 by A49,A53,XBOOLE_1:1;
                     suppose C1 /\ (A1 \/ A2) <> {};
                      then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
                      then Y1 meets (X1 union X2) by A33,Def3;
                     then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/
                      A2) by A33,Def5;
                     then C1 /\ (A1 \/ A2) c= A1 by A30,Th4;
                      hence A1 \/ A2 c= A1 by A49,A54,XBOOLE_1:8;
                     end;
                  hence A1 \/ A2 c= A1;
                 end;
           hence A1 \/ A2 c= A1 by A33,A49,A50;
         end;
          then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by XBOOLE_1:7;
          then A2 c= A1 by XBOOLE_1:1;
          hence contradiction by A29,Th4;
        end;
      then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) &
      the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A33,A34,Def5;
      then A55: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
          now per cases;
            suppose A56: A1 \/ A2 c= C1 \/ C2;
            thus ex C being Subset of X
             st the carrier of X = (C1 \/ C2) \/ C &
                     C /\ (A1 \/ A2) c= A1 /\ A2 & C is open
             proof
              take C = (C1 \/ C2)`;
A57:          C1 \/ C2 is closed by A32,TOPS_1:36;
                C misses (A1 \/ A2) by A56,TOPS_1:20;
              then C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
              hence thesis by A1,A57,PRE_TOPC:18,TOPS_1:29,XBOOLE_1:2;
             end;
            suppose A58: not A1 \/ A2 c= C1 \/ C2;
            thus ex C being Subset of X
            st the carrier of X = (C1 \/ C2) \/ C &
                     C /\ (A1 \/ A2) c= A1 /\ A2 & C is open
             proof
              consider Y being open non empty SubSpace of X such that
                A59: the TopStruct of X = (Y1 union Y2) union Y &
                    Y meet (X1 union X2) is SubSpace of X1 meet X2
                                                      by A31,A33,A58,Th4;
                the carrier of Y is Subset of X by Th1;
             then reconsider C = the carrier of Y as Subset of X;
                A60: C is open by Th16;
                 now assume not Y meets (X1 union X2);
                then A61: C misses (A1 \/ A2) by A33,Def3;
                  the carrier of X = (C1 \/ C2) \/ C by A33,A59,Def2;
                 then A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC
:15
                      .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/
 A2)) by XBOOLE_1:23
                      .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A61,XBOOLE_0:def 7
                      .= (C1 \/ C2) /\ (A1 \/ A2);
                hence contradiction by A58,XBOOLE_1:17;
               end;
              then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) &
                   the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
              then A62: C /\ (A1 \/ A2) c= A1 /\ A2 by A59,Th4;
                the carrier of X = (the carrier of Y1 union Y2) \/ C by A59,
Def2
                              .= (C1 \/ C2) \/ C by Def2;
              hence thesis by A60,A62;
             end;
           end;
         then for A1, A2 be Subset of X holds
 A1 = the carrier of X1 & A2 = the carrier of X2 implies
 A1,A2 are_weakly_separated by A32,A55,Th59;
     hence X1,X2 are_weakly_separated by Def9;
   end;
   hence X1,X2 are_weakly_separated by Th86;
  end;
  hence thesis by A4;
 end;

theorem
   X = X1 union X2 & X1 meets X2 implies
  (X1,X2 are_weakly_separated iff
   (X1 is SubSpace of X2 or X2 is SubSpace of X1 or
     ex Y1, Y2 being closed non empty SubSpace of X st
      Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
       (X = Y1 union Y2 or ex Y being open non empty SubSpace of X st
         X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2)))
 proof assume A1: X = X1 union X2;
    reconsider A1 = the carrier of X1 as Subset of X by Th1;
    reconsider A2 = the carrier of X2 as Subset of X by Th1;
   A2: A1 \/ A2 = the carrier of X by A1,Def2;
   assume A3: X1 meets X2;
  A4:now assume X1,X2 are_weakly_separated;
      then A5: A1,A2 are_weakly_separated by Def9;
       now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
       then not A1 c= A2 & not A2 c= A1 by Th4;
      then consider C1, C2 being non empty Subset of X such that
        A6: C1 is closed & C2 is closed & C1 c= A1 & C2 c= A2 and
        A7: A1 \/ A2 = C1 \/ C2 or
         ex C being non empty Subset of X st
            A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open
                                                         by A2,A5,Th62;
      thus ex Y1, Y2 being closed non empty SubSpace of X
            st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
             (X = Y1 union Y2 or ex Y being open non empty SubSpace of X st
              X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2)
       proof
          consider Y1 being strict closed non empty SubSpace of X such that
            A8: C1 = the carrier of Y1 by A6,Th15;
          consider Y2 being strict closed non empty SubSpace of X such that
            A9: C2 = the carrier of Y2 by A6,Th15;
        take Y1,Y2;
          now assume X <> Y1 union Y2;
         then consider C being non empty Subset of X such that
           A10: A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open
            by A1,A2,A7,A8,A9,Def2;
         thus ex Y being open non empty SubSpace of X st
                X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2
          proof
           consider Y being strict open non empty SubSpace of X such that
            A11: C = the carrier of Y by A10,Th20;
           take Y;
             A12: the carrier of X = (the carrier of Y1 union Y2) \/ C
                                                by A2,A8,A9,A10,Def2
                    .= the carrier of (Y1 union Y2) union Y by A11,Def2;
               C c= the carrier of X1 meet X2 by A3,A10,Def5;
           hence thesis by A1,A11,A12,Th4,Th5;
          end;
        end;
        hence thesis by A6,A8,A9,Th4;
       end;
     end;
     hence X1 is SubSpace of X2 or X2 is SubSpace of X1
           or ex Y1, Y2 being closed non empty SubSpace of X st
            Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
             (X = Y1 union Y2 or ex Y being open non empty SubSpace of X st
              X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2);
    end;
    now assume A13:
        X1 is SubSpace of X2 or X2 is SubSpace of X1
        or (not X1 is SubSpace of X2 & not X2 is SubSpace of X1 implies
         ex Y1, Y2 being closed non empty SubSpace of X st
          Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
          (X = Y1 union Y2 or ex Y being open non empty SubSpace of X st
           X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2));
     now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
    then consider Y1, Y2 being closed non empty SubSpace of X
     such that
       A14: Y1 is SubSpace of X1 & Y2 is SubSpace of X2 and
       A15: X = Y1 union Y2 or ex Y being open non empty SubSpace of X st
           X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 by A13;
       the carrier of Y1 is Subset of X by Th1;
     then reconsider C1 = the carrier of Y1 as Subset of X;
       the carrier of Y2 is Subset of X by Th1;
     then reconsider C2 = the carrier of Y2 as Subset of X;
       A16: C1 is closed & C2 is closed by Th11;
      A17: C1 c= A1 & C2 c= A2 by A14,Th4;
          now per cases;
            suppose A18: A1 \/ A2 = C1 \/ C2;
            thus ex C being Subset of X st
                  A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open
             proof
              take {}X;
              thus thesis by A18,XBOOLE_1:2;
             end;
            suppose A19: A1 \/ A2 <> C1 \/ C2;
            thus ex C being Subset of X st
                  A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is open
             proof
              consider Y being open non empty SubSpace of X such that
                A20: X = (Y1 union Y2) union Y &
                    Y is SubSpace of X1 meet X2 by A2,A15,A19,Def2;
                the carrier of Y is Subset of X by Th1;
              then reconsider C = the carrier of Y as Subset of X;
                A21: C is open by Th16;
                 A1 /\ A2 = the carrier of X1 meet X2 by A3,Def5;
              then A22: C c= A1 /\ A2 by A20,Th4;
                 A1 \/ A2 = (the carrier of Y1 union Y2) \/ C by A2,A20,Def2
                      .= (C1 \/ C2) \/ C by Def2;
              hence thesis by A21,A22;
             end;
           end;

         then for A1, A2 be Subset of X holds
 A1 = the carrier of X1 & A2 = the carrier of X2 implies
 A1,A2 are_weakly_separated by A2,A16,A17,Th61;
     hence X1,X2 are_weakly_separated by Def9;
   end;
   hence X1,X2 are_weakly_separated by Th86;
  end;
  hence thesis by A4;
 end;

theorem
   X = X1 union X2 & X1 misses X2 implies
  (X1,X2 are_weakly_separated iff
    X1 is closed SubSpace of X & X2 is closed SubSpace of X)
 proof
   assume A1: X = X1 union X2;
   assume A2: X1 misses X2;
  thus X1,X2 are_weakly_separated implies
             X1 is closed SubSpace of X & X2 is closed SubSpace of X
   proof
       the carrier of X1 is Subset of X by Th1;
     then reconsider A1 = the carrier of X1 as Subset of X;
       the carrier of X2 is Subset of X by Th1;
     then reconsider A2 = the carrier of X2 as Subset of X;
       A1 \/ A2 = the carrier of X by A1,Def2;
    then A3: A1 \/ A2 = [#]X by PRE_TOPC:12;
    assume X1,X2 are_weakly_separated;
    then X1,X2 are_separated by A2,Th85;
    then A1,A2 are_separated by Def8;
    then A1 is closed & A2 is closed by A3,CONNSP_1:5;
    hence thesis by Th11;
   end;
  thus X1 is closed SubSpace of X & X2 is closed SubSpace of X implies
                                     X1,X2 are_weakly_separated by Th87;
 end;

::Second Characterization of Weakly Separated Subspaces of Topological Spaces.
theorem
   for X being non empty TopSpace, X1,X2 being non empty SubSpace of X holds
  X1 meets X2 implies (X1,X2 are_weakly_separated iff
   (X1 is SubSpace of X2 or X2 is SubSpace of X1 or
     ex Y1, Y2 being open non empty SubSpace of X st
        Y1 meet (X1 union X2) is SubSpace of X1 &
         Y2 meet (X1 union X2) is SubSpace of X2 &
            (X1 union X2 is SubSpace of Y1 union Y2 or
                ex Y being closed non empty SubSpace of X st
                    the TopStruct of X = (Y1 union Y2) union Y &
                      Y meet (X1 union X2) is SubSpace of X1 meet X2)))
 proof let X be non empty TopSpace, X1,X2 be non empty SubSpace of X;
   reconsider A1 = the carrier of X1 as Subset of X by Th1;
   reconsider A2 = the carrier of X2 as Subset of X by Th1;
    A1: [#]X = the carrier of X by PRE_TOPC:12;
    A2: X is SubSpace of X by Th2;
  assume A3: X1 meets X2;
  A4:now assume X1,X2 are_weakly_separated;
      then A5: A1,A2 are_weakly_separated by Def9;
       now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
      then A6: not A1 c= A2 & not A2 c= A1 by Th4;
      then consider C1, C2 being non empty Subset of X such that
        A7: C1 is open & C2 is open and
        A8: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 and
        A9: A1 \/ A2 c= C1 \/ C2 or
            ex C being non empty Subset of X st C is closed &
             C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C
                                                         by A5,Th64;
      A10:now assume C1 misses (A1 \/ A2);
         then A11: C1 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
           now per cases;
          suppose A1 \/ A2 c= C1 \/ C2;
           then A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
                       .= {} \/ (C2 /\ (A1 \/ A2)) by A11,XBOOLE_1:23
                       .= C2 /\ (A1 \/ A2);
           then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by A8,XBOOLE_1:7;
           hence contradiction by A6,XBOOLE_1:1;
          suppose not A1 \/ A2 c= C1 \/ C2;
           then consider C being non empty Subset of X such that
            A12: C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 and
            A13: the carrier of X = (C1 \/ C2) \/ C by A9;
             A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,A13,PRE_TOPC:15
                  .= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
                  .= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A11,XBOOLE_1:23
                  .= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
           then A1 \/ A2 c= A2 \/ A1 /\ A2 & A1 /\ A2 c= A2
             by A8,A12,XBOOLE_1:13,17;
           then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by XBOOLE_1:7,12
;
           hence contradiction by A6,XBOOLE_1:1;
         end;
          hence contradiction;
         end;
      A14:now assume C2 misses (A1 \/ A2);
         then A15: C2 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
           now per cases;
          suppose A1 \/ A2 c= C1 \/ C2;
           then A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
                       .= (C1 /\ (A1 \/ A2)) \/ {} by A15,XBOOLE_1:23
                       .= C1 /\ (A1 \/ A2);
           then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by A8,XBOOLE_1:7;
           hence contradiction by A6,XBOOLE_1:1;
          suppose not A1 \/ A2 c= C1 \/ C2;
           then consider C being non empty Subset of X such that
            A16: C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 and
            A17: the carrier of X = (C1 \/ C2) \/ C by A9;
             A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A1,A17,PRE_TOPC:15
                  .= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
                  .= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A15,XBOOLE_1:23
                  .= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
           then A1 \/ A2 c= A1 \/ A1 /\ A2 & A1 /\ A2 c= A1
                                  by A8,A16,XBOOLE_1:13,17;
           then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by XBOOLE_1:7,12
;
           hence contradiction by A6,XBOOLE_1:1;
         end;
          hence contradiction;
         end;
      thus ex Y1, Y2 being open non empty SubSpace of X st
       Y1 meet (X1 union X2) is SubSpace of X1 &
        Y2 meet (X1 union X2) is SubSpace of X2 &
         (X1 union X2 is SubSpace of Y1 union Y2 or
          ex Y being closed non empty SubSpace of X st
           the TopStruct of X = (Y1 union Y2) union Y &
           Y meet (X1 union X2) is SubSpace of X1 meet X2)
       proof
          consider Y1 being strict open non empty SubSpace of X such that
            A18: C1 = the carrier of Y1 by A7,Th20;
          consider Y2 being strict open non empty SubSpace of X such that
            A19: C2 = the carrier of Y2 by A7,Th20;
        take Y1,Y2;
         A20: the carrier of X1 union X2 = A1 \/ A2 &
              the carrier of Y1 union Y2 = C1 \/ C2 by A18,A19,Def2;
        then Y1 meets (X1 union X2) & Y2 meets (X1 union X2)
                                   by A10,A14,A18,A19,Def3;
        then A21: the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) &
             the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2)
                                                by A18,A19,A20,Def5;
          now assume A22:not X1 union X2 is SubSpace of Y1 union Y2;
         then A23: not A1 \/ A2 c= C1 \/ C2 by A20,Th4;
         consider C being non empty Subset of X such that
          A24: C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 &
               the carrier of X = (C1 \/ C2) \/ C by A9,A20,A22,Th4;
         thus ex Y being closed non empty SubSpace of X st
               the TopStruct of X = (Y1 union Y2) union Y &
               Y meet (X1 union X2) is SubSpace of X1 meet X2
          proof
           consider Y being strict closed non empty SubSpace of X such that
            A25: C = the carrier of Y by A24,Th15;
           take Y;
             A26: the carrier of X = (the carrier of Y1 union Y2) \/ C
                                                    by A18,A19,A24,Def2
                    .= the carrier of (Y1 union Y2) union Y by A25,Def2;
               now assume C misses (A1 \/ A2);
             then A27: C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
                 A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,A24,PRE_TOPC:
15
                      .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A27,XBOOLE_1:23
                      .= (C1 \/ C2) /\ (A1 \/ A2);
              hence contradiction by A23,XBOOLE_1:17;
             end;
            then Y meets (X1 union X2) by A20,A25,Def3;
           then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) &
                the carrier of X1 meet X2 = A1 /\ A2 by A3,A20,A25,Def5;
           hence thesis by A2,A24,A26,Th4,Th5;
          end;
        end;
        hence thesis by A8,A21,Th4;
       end;
     end;
     hence X1 is SubSpace of X2 or X2 is SubSpace of X1
       or ex Y1, Y2 being open non empty SubSpace of X st
        Y1 meet (X1 union X2) is SubSpace of X1 &
         Y2 meet (X1 union X2) is SubSpace of X2 &
          (X1 union X2 is SubSpace of Y1 union Y2
           or ex Y being closed non empty SubSpace of X st
            the TopStruct of X = (Y1 union Y2) union Y &
            Y meet (X1 union X2) is SubSpace of X1 meet X2);
    end;
    now assume A28:
    X1 is SubSpace of X2 or X2 is SubSpace of X1
     or ex Y1, Y2 being open non empty SubSpace of X st
      Y1 meet (X1 union X2) is SubSpace of X1 &
       Y2 meet (X1 union X2) is SubSpace of X2 &
        (X1 union X2 is SubSpace of Y1 union Y2
         or ex Y being closed non empty SubSpace of X st
          the TopStruct of X = (Y1 union Y2) union Y &
          Y meet (X1 union X2) is SubSpace of X1 meet X2);
     now assume A29: not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
    then consider Y1, Y2 being open non empty SubSpace of X
     such that
       A30: Y1 meet (X1 union X2) is SubSpace of X1 &
           Y2 meet (X1 union X2) is SubSpace of X2 and
       A31: X1 union X2 is SubSpace of Y1 union Y2 or
            ex Y being closed non empty SubSpace of X st
             the TopStruct of X = (Y1 union Y2) union Y &
             Y meet (X1 union X2) is SubSpace of X1 meet X2 by A28;
       the carrier of Y1 is Subset of X by Th1;
     then reconsider C1 = the carrier of Y1 as Subset of X;
       the carrier of Y2 is Subset of X by Th1;
     then reconsider C2 = the carrier of Y2 as Subset of X;
       A32: C1 is open & C2 is open by Th16;
      A33: the carrier of X1 union X2 = A1 \/ A2 &
           the carrier of Y1 union Y2 = C1 \/ C2 by Def2;
      A34:now assume Y1 misses (X1 union X2);
          then A35: C1 misses (A1 \/ A2) by A33,Def3;
           now per cases;
          suppose X1 union X2 is SubSpace of Y1 union Y2;
           then A1 \/ A2 c= C1 \/ C2 by A33,Th4;
           then A36: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
                           .= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/
 A2)) by XBOOLE_1:23
                           .= {} \/ (C2 /\ (A1 \/ A2)) by A35,XBOOLE_0:def 7
                           .= C2 /\ (A1 \/ A2);
           then C2 meets (A1 \/ A2) by A33,XBOOLE_0:def 7;
           then Y2 meets (X1 union X2) by A33,Def3;
           then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2)
                                                                by A33,Def5;
           hence A1 \/ A2 c= A2 by A30,A36,Th4;
          suppose not X1 union X2 is SubSpace of Y1 union Y2;
           then consider Y being closed non empty SubSpace of X such that
            A37: the TopStruct of X = (Y1 union Y2) union Y and
            A38: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A31;
           reconsider C = the carrier of Y as Subset of X
           by Th1;
             the carrier of X = (C1 \/ C2) \/ C by A33,A37,Def2;
           then A39:A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC:
15
                     .= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
                     .= (C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/
 A2)) by XBOOLE_1:23
                     .= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A35,XBOOLE_0:def 7
                     .= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
            A40: now assume C2 /\ (A1 \/ A2) <> {};
                  then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y2 meets (X1 union X2) by A33,Def3;
                  then A41: the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/
A2)
                                                                by A33,Def5;
                  then A42: C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
                      now per cases;
                     suppose C /\ (A1 \/ A2) = {};
                      hence A1 \/ A2 c= A2 by A30,A39,A41,Th4;
                     suppose C /\ (A1 \/ A2) <> {};
                      then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                      then Y meets (X1 union X2) by A33,Def3;
                      then the carrier of Y meet (X1 union X2) = C /\ (A1 \/
 A2)
                         & the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
                      then C /\ (A1 \/ A2) c= A1 /\ A2 by A38,Th4;
                      then A1 \/ A2 c= A2 \/ A1 /\ A2 & A1 /\ A2 c= A2
                                            by A39,A42,XBOOLE_1:13,17;
                      hence A1 \/ A2 c= A2 by XBOOLE_1:12;
                     end;
                  hence A1 \/ A2 c= A2;
                 end;
               now assume C /\ (A1 \/ A2) <> {};
                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y meets (X1 union X2) by A33,Def3;
                  then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
                     & the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
                  then A43: C /\ (A1 \/ A2) c= A1 /\ A2 & A1 /\ A2 c= A2
                                                   by A38,Th4,XBOOLE_1:17;
                  then A44: C /\ (A1 \/ A2) c= A2 by XBOOLE_1:1;
                      now per cases;
                     suppose C2 /\ (A1 \/ A2) = {};
                      hence A1 \/ A2 c= A2 by A39,A43,XBOOLE_1:1;
                     suppose C2 /\ (A1 \/ A2) <> {};
                  then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
                      then Y2 meets (X1 union X2) by A33,Def3;
                     then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/
 A2) by A33,Def5;
                     then C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
                      hence A1 \/ A2 c= A2 by A39,A44,XBOOLE_1:8;
                     end;
                  hence A1 \/ A2 c= A2;
                 end;
           hence A1 \/ A2 c= A2 by A33,A39,A40;
         end;
          then A1 \/ A2 c= A2 & A1 c= A1 \/ A2 by XBOOLE_1:7;
          then A1 c= A2 by XBOOLE_1:1;
          hence contradiction by A29,Th4;
         end;
        now assume not Y2 meets (X1 union X2);
          then A45: C2 misses (A1 \/ A2) by A33,Def3;
           now per cases;
          suppose X1 union X2 is SubSpace of Y1 union Y2;
           then A1 \/ A2 c= C1 \/ C2 by A33,Th4;
           then A46: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
                           .= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/
 A2)) by XBOOLE_1:23
                           .= (C1 /\ (A1 \/ A2)) \/ {} by A45,XBOOLE_0:def 7
                           .= C1 /\ (A1 \/ A2);
           then C1 meets (A1 \/ A2) by A33,XBOOLE_0:def 7;
           then Y1 meets (X1 union X2) by A33,Def3;
           then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2)
                                                                by A33,Def5;
           hence A1 \/ A2 c= A1 by A30,A46,Th4;
          suppose not X1 union X2 is SubSpace of Y1 union Y2;
           then consider Y being closed non empty SubSpace of X such that
            A47: the TopStruct of X = (Y1 union Y2) union Y and
            A48: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A31;
           reconsider C = the carrier of Y as Subset of X
           by Th1;
             the carrier of X = (C1 \/ C2) \/ C by A33,A47,Def2;
           then A49:A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC:
15
                     .= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
                     .= (C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/
 A2)) by XBOOLE_1:23
                     .= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A45,XBOOLE_0:def 7
                     .= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
            A50: now assume C1 /\ (A1 \/ A2) <> {};
                  then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y1 meets (X1 union X2) by A33,Def3;
                  then A51: the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/
A2)
                                                                by A33,Def5;
                  then A52: C1 /\ (A1 \/ A2) c= A1 by A30,Th4;
                      now per cases;
                     suppose C /\ (A1 \/ A2) = {};
                      hence A1 \/ A2 c= A1 by A30,A49,A51,Th4;
                     suppose C /\ (A1 \/ A2) <> {};
                      then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                      then Y meets (X1 union X2) by A33,Def3;
                      then the carrier of Y meet (X1 union X2) = C /\ (A1 \/
 A2)
                         & the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
                      then C /\ (A1 \/ A2) c= A1 /\ A2 by A48,Th4;
                      then A1 \/ A2 c= A1 \/ A1 /\ A2 & A1 /\ A2 c= A1
                                              by A49,A52,XBOOLE_1:13,17;
                      hence A1 \/ A2 c= A1 by XBOOLE_1:12;
                     end;
                  hence A1 \/ A2 c= A1;
                 end;
               now assume C /\ (A1 \/ A2) <> {};
                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y meets (X1 union X2) by A33,Def3;
                  then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
                     & the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
                  then A53: C /\ (A1 \/ A2) c= A1 /\ A2 & A1 /\ A2 c= A1
                     by A48,Th4,XBOOLE_1:17;
                  then A54: C /\ (A1 \/ A2) c= A1 by XBOOLE_1:1;
                      now per cases;
                     suppose C1 /\ (A1 \/ A2) = {};
                      hence A1 \/ A2 c= A1 by A49,A53,XBOOLE_1:1;
                     suppose C1 /\ (A1 \/ A2) <> {};
                      then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
                      then Y1 meets (X1 union X2) by A33,Def3;
                     then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/
                      A2) by A33,Def5;
                     then C1 /\ (A1 \/ A2) c= A1 by A30,Th4;
                      hence A1 \/ A2 c= A1 by A49,A54,XBOOLE_1:8;
                     end;
                  hence A1 \/ A2 c= A1;
                 end;
           hence A1 \/ A2 c= A1 by A33,A49,A50;
         end;
          then A1 \/ A2 c= A1 & A2 c= A1 \/ A2 by XBOOLE_1:7;
          then A2 c= A1 by XBOOLE_1:1;
          hence contradiction by A29,Th4;
         end;
      then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) &
      the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A33,A34,Def5;
      then A55: C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2) c= A2 by A30,Th4;
          now per cases;
            suppose A56: A1 \/ A2 c= C1 \/ C2;
            thus ex C being Subset of X
            st the carrier of X = (C1 \/ C2) \/ C &
                     C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed
             proof
              take C = (C1 \/ C2)`;
A57:          C1 \/ C2 is open by A32,TOPS_1:37;
                C misses (A1 \/ A2) by A56,TOPS_1:20;
              then C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
              hence thesis by A1,A57,PRE_TOPC:18,TOPS_1:30,XBOOLE_1:2;
             end;
            suppose A58: not A1 \/ A2 c= C1 \/ C2;
            thus ex C being Subset of X
            st the carrier of X = (C1 \/ C2) \/ C &
                     C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed
             proof
              consider Y being closed non empty SubSpace of X such that
                A59: the TopStruct of X = (Y1 union Y2) union Y &
                    Y meet (X1 union X2) is SubSpace of X1 meet X2
                                                      by A31,A33,A58,Th4;
                the carrier of Y is Subset of X by Th1;
              then reconsider C = the carrier of Y as Subset of X
             ;
                A60: C is closed by Th11;
                 now assume not Y meets (X1 union X2);
                then A61: C misses (A1 \/ A2) by A33,Def3;

                  the carrier of X = (C1 \/ C2) \/ C by A33,A59,Def2;
                then A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A1,PRE_TOPC:
15
                      .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/
 A2)) by XBOOLE_1:23
                      .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A61,XBOOLE_0:def 7
                      .= (C1 \/ C2) /\ (A1 \/ A2);
                hence contradiction by A58,XBOOLE_1:17;
               end;
              then the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) &
                   the carrier of X1 meet X2 = A1 /\ A2 by A3,A33,Def5;
              then A62: C /\ (A1 \/ A2) c= A1 /\ A2 by A59,Th4;
                the carrier of X = (the carrier of Y1 union Y2) \/ C by A59,
Def2
                              .= (C1 \/ C2) \/ C by Def2;
              hence thesis by A60,A62;
             end;
           end;
         then for A1, A2 be Subset of X holds
 A1 = the carrier of X1 & A2 = the carrier of X2 implies
 A1,A2 are_weakly_separated by A32,A55,Th63;
     hence X1,X2 are_weakly_separated by Def9;
   end;
   hence X1,X2 are_weakly_separated by Th86;
  end;
  hence thesis by A4;
 end;

theorem
   X = X1 union X2 & X1 meets X2 implies
  (X1,X2 are_weakly_separated iff
   (X1 is SubSpace of X2 or X2 is SubSpace of X1 or
    ex Y1, Y2 being open non empty SubSpace of X st
     Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
      (X = Y1 union Y2 or ex Y being closed non empty SubSpace of X st
        X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2)))
 proof
   assume A1: X = X1 union X2;
    reconsider A1 = the carrier of X1 as Subset of X by Th1;
    reconsider A2 = the carrier of X2 as Subset of X by Th1;
   A2: A1 \/ A2 = the carrier of X by A1,Def2;
   assume A3: X1 meets X2;
  A4:now assume X1,X2 are_weakly_separated;
      then A5: A1,A2 are_weakly_separated by Def9;
       now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
       then not A1 c= A2 & not A2 c= A1 by Th4;
      then consider C1, C2 being non empty Subset of X such that
        A6: C1 is open & C2 is open & C1 c= A1 & C2 c= A2 and
        A7: A1 \/ A2 = C1 \/ C2 or
        ex C being non empty Subset of X st
            A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed
                                                        by A2,A5,Th66;
      thus ex Y1, Y2 being open non empty SubSpace of X
            st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
             (X = Y1 union Y2 or ex Y being closed non empty SubSpace of X st
              X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2)
       proof
          consider Y1 being strict open non empty SubSpace of X such that
            A8: C1 = the carrier of Y1 by A6,Th20;
          consider Y2 being strict open non empty SubSpace of X such that
            A9: C2 = the carrier of Y2 by A6,Th20;
        take Y1,Y2;
          now assume X <> Y1 union Y2;
         then consider C being non empty Subset of X such that
           A10: A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed
                                             by A1,A2,A7,A8,A9,Def2;
         thus ex Y being closed non empty SubSpace of X st
                X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2
          proof
           consider Y being strict closed non empty SubSpace of X such that
            A11: C = the carrier of Y by A10,Th15;
           take Y;
              A12: the carrier of X = (the carrier of Y1 union Y2) \/ C
                                                by A2,A8,A9,A10,Def2
                    .= the carrier of (Y1 union Y2) union Y by A11,Def2;

               C c= the carrier of X1 meet X2 by A3,A10,Def5;
            hence thesis by A1,A11,A12,Th4,Th5;
          end;
        end;
        hence thesis by A6,A8,A9,Th4;
       end;
    end;
    hence X1 is SubSpace of X2 or X2 is SubSpace of X1 or
          ex Y1, Y2 being open non empty SubSpace of X st
           Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
            (X = Y1 union Y2 or ex Y being closed non empty SubSpace of X st
             X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2);
    end;
    now assume A13:
        X1 is SubSpace of X2 or X2 is SubSpace of X1 or
        ex Y1, Y2 being open non empty SubSpace of X st
         Y1 is SubSpace of X1 & Y2 is SubSpace of X2 &
         (X = Y1 union Y2 or ex Y being closed non empty SubSpace of X st
          X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2);
     now assume not X1 is SubSpace of X2 & not X2 is SubSpace of X1;
    then consider Y1, Y2 being open non empty SubSpace of X such that
       A14: Y1 is SubSpace of X1 & Y2 is SubSpace of X2 and
       A15: X = Y1 union Y2 or ex Y being closed non empty SubSpace of X st
           X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 by A13;
       the carrier of Y1 is Subset of X by Th1;
     then reconsider C1 = the carrier of Y1 as Subset of X;
       the carrier of Y2 is Subset of X by Th1;
     then reconsider C2 = the carrier of Y2 as Subset of X;
       A16: C1 is open & C2 is open by Th16;
      A17: C1 c= A1 & C2 c= A2 by A14,Th4;
          now per cases;
            suppose A18: A1 \/ A2 = C1 \/ C2;
            thus ex C being Subset of X st
                  A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed
             proof
              take {}X;
              thus thesis by A18,XBOOLE_1:2;
             end;
            suppose A19: A1 \/ A2 <> C1 \/ C2;
            thus ex C being Subset of X st
                  A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1 /\ A2 & C is closed
             proof
              consider Y being closed non empty SubSpace of X such that
                A20: X = (Y1 union Y2) union Y &
                    Y is SubSpace of X1 meet X2 by A2,A15,A19,Def2;
                the carrier of Y is Subset of X by Th1;
              then reconsider C = the carrier of Y as Subset of X
             ;
                A21: C is closed by Th11;
                 A1 /\ A2 = the carrier of X1 meet X2 by A3,Def5;
              then A22: C c= A1 /\ A2 by A20,Th4;
                 A1 \/ A2 = (the carrier of Y1 union Y2) \/ C by A2,A20,Def2
                      .= (C1 \/ C2) \/ C by Def2;
              hence thesis by A21,A22;
             end;
           end;
         then for A1, A2 be Subset of X holds
 A1 = the carrier of X1 & A2 = the carrier of X2 implies
 A1,A2 are_weakly_separated by A2,A16,A17,Th65;
     hence X1,X2 are_weakly_separated by Def9;
   end;
   hence X1,X2 are_weakly_separated by Th86;
  end;
  hence thesis by A4;
 end;

theorem
   X = X1 union X2 & X1 misses X2 implies
  (X1,X2 are_weakly_separated iff
    X1 is open SubSpace of X & X2 is open SubSpace of X)
 proof
   assume A1: X = X1 union X2;
   assume A2: X1 misses X2;
  thus X1,X2 are_weakly_separated implies
             X1 is open SubSpace of X & X2 is open SubSpace of X
   proof
       the carrier of X1 is Subset of X by Th1;
     then reconsider A1 = the carrier of X1 as Subset of X;
       the carrier of X2 is Subset of X by Th1;
     then reconsider A2 = the carrier of X2 as Subset of X;
       A1 \/ A2 = the carrier of X by A1,Def2;
    then A3: A1 \/ A2 = [#]X by PRE_TOPC:12;
    assume X1,X2 are_weakly_separated;
    then X1,X2 are_separated by A2,Th85;
    then A1,A2 are_separated by Def8;
    then A1 is open & A2 is open by A3,CONNSP_1:5;
    hence thesis by Th16;
   end;
  thus X1 is open SubSpace of X & X2 is open SubSpace of X implies
                                     X1,X2 are_weakly_separated by Th88;
 end;

::A Characterization of Separated Subspaces by means of Weakly Separated ones.
theorem
   X1,X2 are_separated iff ex Y1, Y2 being non empty SubSpace of X st
  Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &
   (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
 proof
  thus X1,X2 are_separated implies ex Y1, Y2 being non empty SubSpace of X st
    Y1,Y2 are_weakly_separated & X1 is SubSpace of Y1 & X2 is SubSpace of Y2
     & (Y1 misses Y2 or Y1 meet Y2 misses X1 union X2)
   proof assume X1,X2 are_separated;
    then consider Y1, Y2 being open non empty SubSpace of X
    such that A1: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
              A2: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2 by Th83;
    take Y1,Y2;
    thus thesis by A1,A2,Th88;
   end;
  given Y1, Y2 being non empty SubSpace of X such that
    A3: Y1,Y2 are_weakly_separated and
    A4: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
    A5: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
     reconsider C1 = the carrier of Y1 as Subset of X by Th1;
     reconsider C2 = the carrier of Y2 as Subset of X by Th1;
    now let A1, A2 be Subset of X such that
    A6: A1 = the carrier of X1 & A2 = the carrier of X2;
     now per cases;
    suppose Y1 misses Y2;
     then Y1,Y2 are_separated by A3,Th85;
     then A7:     C1,C2 are_separated & A1 c= C1 & A2 c= C2 by A4,A6,Def8,Th4;
     thus A1,A2 are_separated by A7,CONNSP_1:8;
    suppose A8: not Y1 misses Y2;
       ex B1, B2 being Subset of X st
     B1,B2 are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/
 A2
      proof
       take C1,C2;
         the carrier of Y1 meet Y2 = C1 /\ C2 &
                the carrier of X1 union X2 = A1 \/ A2 by A6,A8,Def2,Def5;
       hence thesis by A3,A4,A5,A6,A8,Def3,Def9,Th4;
      end;
     hence A1,A2 are_separated by Th67;
   end;
   hence A1,A2 are_separated;
  end;
  hence X1,X2 are_separated by Def8;
 end;

Back to top