TSEP_1

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

environ

 vocabularies SUBSET_1, XBOOLE_0, TARSKI, PRE_TOPC, STRUCT_0, RELAT_1, RCOMP_1,
      SETFAM_1, CONNSP_1, TSEP_1;
 notations TARSKI, XBOOLE_0, SUBSET_1, STRUCT_0, PRE_TOPC, CONNSP_1, BORSUK_1;
 constructors CONNSP_1, BORSUK_1;
 registrations XBOOLE_0, STRUCT_0, PRE_TOPC, TOPS_1, BORSUK_1;
 requirements BOOLE, SUBSET;
 definitions PRE_TOPC;
 equalities SUBSET_1, STRUCT_0;
 expansions 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
A1: B c= C by XBOOLE_1:37;
  C misses (D \ C) by XBOOLE_1:79;
  hence thesis by A1,XBOOLE_1:63;
end;

Lm2: for A,B,C being set holds (A /\ B) \ C = (A \ C) /\ (B \ C)
proof
  let A,B,C be set;
A1: (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 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 A1,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 4;
  A c= [#]X;
  hence thesis;
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,XBOOLE_1:28;
    end;
    thus thesis by XBOOLE_1:28;
  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 5;
  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: A2 = [#]X2;
  thus the carrier of X1 c= the carrier of X2 implies X1 is SubSpace of X2
  proof
    assume
A3: 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
A4:     R in the topology of X and
A5:     P = R /\ A1 by A1,PRE_TOPC:def 4;
        reconsider Q = R /\ A2 as Subset of X2 by XBOOLE_1:17;
        take Q;
        thus Q in the topology of X2 by A2,A4,PRE_TOPC:def 4;
        Q /\ A1 = R /\ (A2 /\ A1) by XBOOLE_1:16
          .= R /\ A1 by A3,XBOOLE_1:28;
        hence thesis by A5;
      end;
      given Q being Subset of X2 such that
A6:   Q in the topology of X2 and
A7:   P = Q /\ A1;
      consider R being Subset of X such that
A8:   R in the topology of X and
A9:   Q = R /\ [#]X2 by A6,PRE_TOPC:def 4;
      P = R /\ (A2 /\ A1) by A7,A9,XBOOLE_1:16
        .= R /\ A1 by A3,XBOOLE_1:28;
      hence thesis by A1,A8,PRE_TOPC:def 4;
    end;
    hence thesis by A1,A2,A3,PRE_TOPC:def 4;
  end;
  thus thesis by A1,A2,PRE_TOPC:def 4;
end;

Lm3: 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: [#] (X0) = the carrier of X0;
    hence [#](S) c= [#](X) by PRE_TOPC:def 4;
    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 4;
    given Q being Subset of X such that
A2: Q in the topology of X & P = Q /\ [#](S);
    thus thesis by A1,A2,PRE_TOPC:def 4;
  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;
  reconsider S1 = the TopStruct of X1, S2 = the TopStruct of X2 as strict
  SubSpace of X by Lm3;
  set A1 = the carrier of X1, A2 = the carrier of X2;
  assume
A1: A1 = A2;
A2: A1 = [#]S1;
A3: A2 = [#]S2;
  reconsider A1 as Subset of X by BORSUK_1:1;
  S1 = X|(A1) by A2,PRE_TOPC:def 5;
  hence thesis by A1,A3,PRE_TOPC:def 5;
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: [#]X2 c= [#]X1 by PRE_TOPC:def 4;
  [#]X1 c= [#]X by PRE_TOPC:def 4;
  hence [#](X2) c= [#](X) by A1,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 4;
      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 4;
      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 R = Q /\ [#]X1 as Subset of X1;
    reconsider Q1 = Q as Subset of X;
    Q1 is open by A6;
    then
A8: R is open by TOPS_2:24;
    R /\ [#]X2 = Q /\ ([#]X1 /\ [#]X2) by XBOOLE_1:16
      .= P by A1,A7,XBOOLE_1:28;
    then P1 is open by A8,TOPS_2:24;
    hence thesis;
  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:13;
    A c= F by A4,A6,XBOOLE_1:17;
    then
A7: A c= F /\ C by A3,XBOOLE_1:19;
    F /\ C c= A by A2,A4,A6,XBOOLE_1:26;
    hence thesis by A1,A5,A7,XBOOLE_0:def 10;
  end;
  thus thesis by A4,TOPS_2:26;
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:24;
    A c= F by A4,A6,XBOOLE_1:17;
    then
A7: A c= F /\ C by A3,XBOOLE_1:19;
    F /\ C c= A by A2,A4,A6,XBOOLE_1:26;
    hence thesis by A1,A5,A7,XBOOLE_0:def 10;
  end;
  thus thesis by A4,TOPS_2:25;
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 5;
  hence thesis;
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 11;
  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 11;
  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;
  reconsider C = the carrier of X0 as Subset of X by Th1;
  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
    reconsider C = [#]X1 as Subset of X by BORSUK_1:1;
    let B be Subset of X;
    assume
A1: B = the carrier of X2;
    then reconsider BB = B as Subset of X1 by BORSUK_1:1;
    BB is closed by A1,BORSUK_1:def 11;
    then
A2: ex A being Subset of X st A is closed & A /\ [#]X1 = BB by PRE_TOPC:13;
    C is closed by BORSUK_1:def 11;
    hence B is closed by A2;
  end;
  hence thesis by Th7,BORSUK_1:def 11;
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 reconsider A = C as Subset of X by BORSUK_1:1;
A2: A /\ [#]X2 = C by XBOOLE_1:28;
    A is closed by A1,Th11;
    hence C is closed by A2,PRE_TOPC:13;
  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;

Lm4: for T being TopStruct holds the TopStruct of T is SubSpace of T
proof
  let T be TopStruct;
  set S = the TopStruct of T;
  thus [#]S c= [#]T;
  let P be Subset of S;
  hereby
    reconsider Q = P as Subset of T;
    assume
A1: P in the topology of S;
    take Q;
    thus Q in the topology of T by A1;
    thus P = Q /\ [#]S by XBOOLE_1:28;
  end;
  given Q being Subset of T such that
A2: Q in the topology of T & P = Q /\ [#]S;
  thus thesis by A2,XBOOLE_1:28;
end;

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

registration
  let X be non empty TopSpace;
  cluster strict open non empty for 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) .= [#] X by PRE_TOPC:def 5;
      hence thesis;
    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;
  reconsider C = the carrier of X0 as Subset of X by Th1;
  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
    reconsider C = [#]X1 as Subset of X by BORSUK_1:1;
    let B be Subset of X;
    assume
A1: B = the carrier of X2;
    then reconsider BB = B as Subset of X1 by BORSUK_1:1;
    BB is open by A1,Def1;
    then
A2: ex A being Subset of X st A is open & A /\ [#]X1 = BB by TOPS_2:24;
    C is open by Def1;
    hence B is open by A2;
  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 reconsider A = C as Subset of X by BORSUK_1:1;
A2: A /\ [#]X2 = C by XBOOLE_1:28;
    A is open by A1,Th16;
    hence C is open by A2,TOPS_2:24;
  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;
    take X|A;
    thus the carrier of (X|A) = [#](X|A)
      .= (the carrier of X1) \/ (the carrier of X2) by PRE_TOPC:def 5;
  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 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:   A1 \/ A2 = the carrier of the TopStruct of X2 by BORSUK_1:1,XBOOLE_1:12;
      the TopStruct of X2 is strict SubSpace of X by Lm3;
      hence thesis by A1,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 thesis 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;
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  reconsider A = the carrier of X1 union X2 as Subset of X by Th1;
  A1 is closed & A2 is closed by Th11;
  then A1 \/ A2 is closed;
  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;
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  reconsider A = the carrier of X1 union X2 as Subset of X by Th1;
  A1 is open & A2 is open by Th16;
  then A1 \/ A2 is open;
  then A is open by Def2;
  hence thesis by Th16;
end;

definition
  let X1, X2 be 1-sorted;
  pred X1 misses X2 means

  the carrier of X1 misses the carrier of X2;
  correctness;
  symmetry;
end;

notation
  let X1, X2 be 1-sorted;
  antonym X1 meets X2 for X1 misses X2;
end;

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

  func X1 meet X2 -> strict non empty SubSpace of X means
  :Def4:
  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;
    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)
      .= (the carrier of X1) /\ (the carrier of X2) by PRE_TOPC:def 5;
  end;
  uniqueness by Th5;
end;

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

::Properties of the Meet of two Subspaces.

theorem Th26:
  (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 Def4
      .= the carrier of X2 meet X1 by A1,Def4;
    hence thesis by Th5;
  end;
  now
A2: now
      assume that
A3:   X1 meets X2 and
A4:   (X1 meet X2) meets X3;
      (the carrier of X1 meet X2) meets (the carrier of X3) by A4;
      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 A3,Def4;
      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;
      then
      (the carrier of X1) /\ (the carrier of X2 meet X3) <> {} by A5,Def4;
      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 A3,A4,A6;
    end;
    assume
A7: X1 meets X2 & (X1 meet X2) meets X3 or X2 meets X3 & X1 meets (X2 meet X3);
A8: now
      assume that
A9:   X2 meets X3 and
A10:  X1 meets (X2 meet X3);
      (the carrier of X1) meets (the carrier of X2 meet X3) by A10;
      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 A9,Def4;
      then
A11:  ((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
A12:  (the carrier of X1) meets (the carrier of X2) by XBOOLE_0:def 7;
      then X1 meets X2;
      then
      (the carrier of X1 meet X2) /\ (the carrier of X3) <> {} by A11,Def4;
      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 A9,A10,A12;
    end;
    then the carrier of (X1 meet X2) meet X3 = (the carrier of X1 meet X2) /\
    (the carrier of X3) by A7,Def4
      .= ((the carrier of X1) /\ (the carrier of X2)) /\ (the carrier of X3)
    by A7,A8,Def4
      .= (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 A7,A2,Def4
      .= the carrier of X1 meet (X2 meet X3) by A7,A2,Def4;
    hence (X1 meet X2) meet X3 = X1 meet (X2 meet X3) by Th5;
  end;
  hence thesis;
end;

theorem Th27:
  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 Def4;
  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;
  set A1 = the carrier of X1, A2 = the carrier of X2;
  assume
A1: X1 meets 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
A2:   A1 /\ A2 = the carrier of the TopStruct of X1 by BORSUK_1:1,XBOOLE_1:28;
      the TopStruct of X1 is strict SubSpace of X by Lm3;
      hence thesis by A1,A2,Def4;
    end;
    assume X1 meet X2 = the TopStruct of X1;
    then A1 /\ A2 = A1 by A1,Def4;
    then A1 c= A2 by XBOOLE_1:17;
    hence thesis 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
A3:   A1 /\ A2 = the carrier of the TopStruct of X2 by BORSUK_1:1,XBOOLE_1:28;
      the TopStruct of X2 is strict SubSpace of X by Lm3;
      hence thesis by A1,A3,Def4;
    end;
    assume X1 meet X2 = the TopStruct of X2;
    then A1 /\ A2 = A2 by A1,Def4;
    then A2 c= A1 by XBOOLE_1:17;
    hence thesis 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;
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  reconsider A = the carrier of X1 meet X2 as Subset of X by Th1;
  A1 is closed & A2 is closed by Th11;
  then A1 /\ A2 is closed;
  then A is closed by A1,Def4;
  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;
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  reconsider A = the carrier of X1 meet X2 as Subset of X by Th1;
  A1 is open & A2 is open by Th16;
  then A1 /\ A2 is open;
  then A is open by A1,Def4;
  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 Th27;
  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 that
A1: X1 meets Y and
A2: Y meets X2;
  X1 is SubSpace of X1 union X2 by Th22;
  then
A3: the carrier of X1 c= the carrier of X1 union X2 by Th4;
  (the carrier of X1) meets (the carrier of Y) by A1;
  then (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 A3,
XBOOLE_1:3,26;
  then (the carrier of X1 union X2) meets (the carrier of Y) by XBOOLE_0:def 7;
  then
A4: (X1 union X2) meets Y;
  then
  the carrier of (X1 union X2) meet Y = (the carrier of X1 union X2) /\ (
  the carrier of Y) by Def4
    .= ((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,Def4
    .= (the carrier of X1 meet Y) \/ (the carrier of X2 meet Y) by A2,Def4
    .= the carrier of (X1 meet Y) union (X2 meet Y) by Def2;
  hence (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y) by Th5;
  hence Y meet (X1 union X2) = (X1 meet Y) union (X2 meet Y) by A4,Th26
    .= (Y meet X1) union (X2 meet Y) by A1,Th26
    .= (Y meet X1) union (Y meet X2) by A2,Th26;
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 X2 union Y by Th22;
  then
A2: the carrier of Y c= the carrier of X2 union Y by Th4;
  Y is SubSpace of X1 union Y by Th22;
  then the carrier of Y c= the carrier of X1 union Y by Th4;
  then (the carrier of X1 union Y) /\ (the carrier of X2 union Y) <> {} by A2,
XBOOLE_1:3,19;
  then (the carrier of X1 union Y) meets (the carrier of X2 union Y) by
XBOOLE_0:def 7;
  then
A3: (X1 union Y) meets (X2 union Y);
A4: 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
,Def4
    .= ((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 A3,Def4;
  hence (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) by Th5;
  thus thesis by A4,Th5;
end;

begin

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

notation
  let X be TopStruct, A1, A2 be Subset of X;
  antonym A1,A2 are_not_separated for A1,A2 are_separated;
end;

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

::Properties of Separated Subsets of Topological Spaces.

theorem Th34:
  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:22;
    hence thesis by A2,CONNSP_1:def 1;
  end;
  thus thesis by CONNSP_1:1;
end;

theorem Th35:
  A1 \/ A2 is closed & A1,A2 are_separated implies A1 is closed & A2 is closed
proof
  assume
A1: A1 \/ A2 is closed;
  then Cl A1 c= A1 \/ A2 by TOPS_1:5,XBOOLE_1:7;
  then
A2: Cl A1 \ A2 c= A1 by XBOOLE_1:43;
  assume
A3: A1,A2 are_separated;
  then Cl A1 misses A2 by CONNSP_1:def 1;
  then
A4: Cl A1 c= A1 by A2,XBOOLE_1:83;
  Cl A2 c= A1 \/ A2 by A1,TOPS_1:5,XBOOLE_1:7;
  then
A5: Cl A2 \ A1 c= A2 by XBOOLE_1:43;
  Cl A2 misses A1 by A3,CONNSP_1:def 1;
  then
A6: Cl A2 c= A2 by A5,XBOOLE_1:83;
  A1 c= Cl A1 & A2 c= Cl A2 by PRE_TOPC:18;
  hence thesis by A6,A4,XBOOLE_0:def 10;
end;

theorem Th36:
  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
A2: A1 is open;
    A2 c= A1` by A1,SUBSET_1:23;
    then Cl A2 c= A1` by A2,TOPS_1:5;
    then Cl A2 misses A1`` by SUBSET_1:24;
    hence thesis;
  end;
end;

theorem Th37:
  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,Th36;
    hence thesis by CONNSP_1:def 1;
  end;
  thus thesis by CONNSP_1:1;
end;

theorem Th38:
  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 by PRE_TOPC:18;
  assume
A3: A1,A2 are_separated;
  then A2 misses Cl A1 by CONNSP_1:def 1;
  then
A4: A2 c= (Cl A1)` by SUBSET_1:23;
  A1 misses Cl A2 by A3,CONNSP_1:def 1;
  then
A5: A1 c= (Cl A2)` by SUBSET_1:23;
A6: A2 c= Cl A2 by PRE_TOPC:18;
A7: (A1 \/ A2) /\ (Cl A2)` = (A1 \/ A2) \ Cl A2 by SUBSET_1:13
    .= (A1 \ Cl A2) \/ (A2 \ Cl A2) by XBOOLE_1:42
    .= (A1 \ Cl A2) \/ {} by A6,XBOOLE_1:37
    .= A1 /\ (Cl A2)` by SUBSET_1:13
    .= A1 by A5,XBOOLE_1:28;
  (A1 \/ A2) /\ (Cl A1)` = (A1 \/ A2) \ Cl A1 by SUBSET_1:13
    .= (A1 \ Cl A1) \/ (A2 \ Cl A1) by XBOOLE_1:42
    .= {} \/ (A2 \ Cl A1) by A2,XBOOLE_1:37
    .= A2 /\ (Cl A1)` by SUBSET_1:13
    .= A2 by A4,XBOOLE_1:28;
  hence thesis by A1,A7;
end;

::A Restriction Theorem for Separated Subsets (see also CONNSP_1:8).

reserve A1,A2 for Subset of X;

theorem Th39:
  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;
A1: A1 /\ C c= A1 & A2 /\ C c= A2 by XBOOLE_1:17;
  assume A1,A2 are_separated;
  hence thesis by A1,CONNSP_1:7;
end;

theorem Th40:
  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
A1: now
A2:   A1 /\ A2 c= A2 by XBOOLE_1:17;
      assume A2,B are_separated;
      hence thesis by A2,CONNSP_1:7;
    end;
A3: now
A4:   A1 /\ A2 c= A1 by XBOOLE_1:17;
      assume A1,B are_separated;
      hence thesis by A4,CONNSP_1:7;
    end;
    assume A1,B are_separated or A2,B are_separated;
    hence thesis by A3,A1;
  end;
end;

theorem Th41:
  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;
  A1 \/ A2,B are_separated implies A1,B are_separated & A2,B are_separated
  proof
A1: A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7;
    assume A1 \/ A2,B are_separated;
    hence thesis by A1,CONNSP_1:7;
  end;
  hence
  A1,B are_separated & A2,B are_separated iff A1 \/ A2,B are_separated by
CONNSP_1:8;
end;

theorem Th42:
  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:18;
  end;
  given C1, C2 being Subset of X such that
A2: A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed &
  C2 is closed;
  Cl A1 misses A2 & A1 misses Cl A2 by A2,TOPS_1:5,XBOOLE_1:63;
  hence thesis by CONNSP_1:def 1;
end;

::First Characterization of Separated Subsets of Topological Spaces.

theorem Th43:
  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 Th42;
    take C1,C2;
    C1 /\ C2 misses A1 & C1 /\ C2 misses A2 by A2,XBOOLE_1:17,63;
    hence thesis by A1,A3,XBOOLE_1:70;
  end;
  given C1, C2 being Subset of X such that
A4: A1 c= C1 and
A5: A2 c= C2 and
A6: C1 /\ C2 misses A1 \/ A2 and
A7: 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;
A8: now
      A1 /\ C2 c= C1 /\ C2 & A1 /\ C2 c= A1 by A4,XBOOLE_1:17,26;
      then
A9:   A1 /\ C2 c= (C1 /\ C2) /\ A1 by XBOOLE_1:19;
      assume C2 meets A1;
      then
A10:  A1 /\ C2 <> {} by XBOOLE_0:def 7;
      (C1 /\ C2) /\ A1 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:7,26;
      then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A10,A9,XBOOLE_1:1,3;
      hence contradiction by A6,XBOOLE_0:def 7;
    end;
    now
      C1 /\ A2 c= C1 /\ C2 & C1 /\ A2 c= A2 by A5,XBOOLE_1:17,26;
      then
A11:  C1 /\ A2 c= (C1 /\ C2) /\ A2 by XBOOLE_1:19;
      assume C1 meets A2;
      then
A12:  C1 /\ A2 <> {} by XBOOLE_0:def 7;
      (C1 /\ C2) /\ A2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:7,26;
      then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A12,A11,XBOOLE_1:1,3;
      hence contradiction by A6,XBOOLE_0:def 7;
    end;
    hence thesis by A4,A5,A7,A8;
  end;
  hence thesis by Th42;
end;

theorem Th44:
  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 & C1 misses A2 & C2 misses A1 & C1 is closed &
    C2 is closed by Th42;
    take C2`,C1`;
    thus thesis by A1,SUBSET_1:23,24;
  end;
  given C1, C2 being Subset of X such that
A2: A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & 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 A2,SUBSET_1:23,24;
  end;
  hence thesis by Th42;
end;

::Second Characterization of Separated Subsets of Topological Spaces.

theorem Th45:
  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 Th44;
    take C1,C2;
    C1 /\ C2 misses A1 & C1 /\ C2 misses A2 by A2,XBOOLE_1:17,63;
    hence thesis by A1,A3,XBOOLE_1:70;
  end;
  given C1, C2 being Subset of X such that
A4: A1 c= C1 and
A5: A2 c= C2 and
A6: C1 /\ C2 misses A1 \/ A2 and
A7: 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;
A8: now
      A1 /\ C2 c= C1 /\ C2 & A1 /\ C2 c= A1 by A4,XBOOLE_1:17,26;
      then
A9:   A1 /\ C2 c= (C1 /\ C2) /\ A1 by XBOOLE_1:19;
      assume C2 meets A1;
      then
A10:  A1 /\ C2 <> {} by XBOOLE_0:def 7;
      (C1 /\ C2) /\ A1 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:7,26;
      then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A10,A9,XBOOLE_1:1,3;
      hence contradiction by A6,XBOOLE_0:def 7;
    end;
    now
      C1 /\ A2 c= C1 /\ C2 & C1 /\ A2 c= A2 by A5,XBOOLE_1:17,26;
      then
A11:  C1 /\ A2 c= (C1 /\ C2) /\ A2 by XBOOLE_1:19;
      assume C1 meets A2;
      then
A12:  C1 /\ A2 <> {} by XBOOLE_0:def 7;
      (C1 /\ C2) /\ A2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:7,26;
      then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A12,A11,XBOOLE_1:1,3;
      hence contradiction by A6,XBOOLE_0:def 7;
    end;
    hence thesis by A4,A5,A7,A8;
  end;
  hence thesis by Th44;
end;

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

  pred A1,A2 are_weakly_separated means

  A1 \ A2,A2 \ A1 are_separated;
  symmetry;
end;

notation
  let X be TopStruct, A1, A2 be Subset of X;
  antonym A1,A2 are_not_weakly_separated for A1,A2 are_weakly_separated;
end;

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

::Properties of Weakly Separated Subsets of Topological Spaces.

theorem Th46:
  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 that
A1: A1 misses A2 and
A2: A1,A2 are_weakly_separated;
    A1 \ A2 = A1 & A2 \ A1 = A2 by A1,XBOOLE_1:83;
    hence thesis by A2;
  end;
  assume
A3: A1,A2 are_separated;
  then A1 misses A2 by CONNSP_1:1;
  then A1 \ A2 = A1 & A2 \ A1 = A2 by XBOOLE_1:83;
  hence thesis by A3,CONNSP_1:1;
end;

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

theorem Th48:
  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 that
A1: A1 is closed and
A2: A2 is closed;
  Cl(A2 \ A1) c= A2 by A2,TOPS_1:5,XBOOLE_1:36;
  then Cl(A2 \ A1) \ A2 = {} by XBOOLE_1:37;
  then
A3: (A1 \ A2) misses Cl(A2 \ A1) by Lm1;
  Cl(A1 \ A2) c= A1 by A1,TOPS_1:5,XBOOLE_1:36;
  then Cl(A1 \ A2) \ A1 = {} by XBOOLE_1:37;
  then Cl(A1 \ A2) misses (A2 \ A1) by Lm1;
  then A1 \ A2,A2 \ A1 are_separated by A3,CONNSP_1:def 1;
  hence thesis;
end;

theorem Th49:
  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 that
A1: A1 is open and
A2: A2 is open;
  (A2 \ A1) misses A1 by XBOOLE_1:79;
  then Cl(A2 \ A1) misses A1 by A1,Th36;
  then
A3: (A1 \ A2) misses Cl(A2 \ A1) by XBOOLE_1:36,63;
  A2 misses (A1 \ A2) by XBOOLE_1:79;
  then A2 misses Cl(A1 \ A2) by A2,Th36;
  then Cl(A1 \ A2) misses (A2 \ A1) by XBOOLE_1:36,63;
  then A1 \ A2,A2 \ A1 are_separated by A3,CONNSP_1:def 1;
  hence thesis;
end;

::Extension Theorems for Weakly Separated Subsets.

theorem Th50:
  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;
  (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;
  then
A1: (A1 \/ C) \ (A2 \/ C) c= A1 \ A2 by XBOOLE_1:17;
  (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
A2: (A2 \/ C) \ (A1 \/ C) c= A2 \ A1 by XBOOLE_1:17;
  assume A1,A2 are_weakly_separated;
  then A1 \ A2,A2 \ A1 are_separated;
  then (A1 \/ C) \ (A2 \/ C),(A2 \/ C) \ (A1 \/ C) are_separated by A1,A2,
CONNSP_1:7;
  hence thesis;
end;

theorem Th51:
  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 and
A2: B2 c= A1;
  A2 c= A2 \/ B2 by XBOOLE_1:7;
  then B1 c= A2 \/ B2 by A1,XBOOLE_1:1;
  then
A3: B1 \ (A2 \/ B2) = {} by XBOOLE_1:37;
  A1 c= A1 \/ B1 by XBOOLE_1:7;
  then B2 c= A1 \/ B1 by A2,XBOOLE_1:1;
  then
A4: B2 \ (A1 \/ B1) = {} by XBOOLE_1:37;
  (A2 \/ B2) \ (A1 \/ B1) = (A2 \ (A1 \/ B1)) \/ (B2 \ (A1 \/ B1)) by
XBOOLE_1:42;
  then
A5: (A2 \/ B2) \ (A1 \/ B1) c= A2 \ A1 by A4,XBOOLE_1:7,34;
  (A1 \/ B1) \ (A2 \/ B2) = (A1 \ (A2 \/ B2)) \/ (B1 \ (A2 \/ B2)) by
XBOOLE_1:42;
  then
A6: (A1 \/ B1) \ (A2 \/ B2) c= A1 \ A2 by A3,XBOOLE_1:7,34;
  assume A1,A2 are_weakly_separated;
  then A1 \ A2,A2 \ A1 are_separated;
  then (A1 \/ B1) \ (A2 \/ B2),(A2 \/ B2) \ (A1 \/ B1) are_separated by A6,A5,
CONNSP_1:7;
  hence thesis;
end;

theorem Th52:
  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 that
A1: A1,B are_weakly_separated and
A2: A2,B are_weakly_separated;
    A2 \ B,B \ A2 are_separated by A2;
    then
A3: (A1 \ B) /\ (A2 \ B),B \ A2 are_separated by Th40;
    A1 \ B,B \ A1 are_separated by A1;
    then (A1 \ B) /\ (A2 \ B),B \ A1 are_separated by Th40;
    then (A1 \ B) /\ (A2 \ B),(B \ A1) \/ (B \ A2) are_separated by A3,Th41;
    then (A1 /\ A2) \ B,(B \ A1) \/ (B \ A2) are_separated by Lm2;
    then (A1 /\ A2) \ B,B \ (A1 /\ A2) are_separated by XBOOLE_1:54;
    hence thesis;
  end;
end;

theorem Th53:
  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 that
A1: A1,B are_weakly_separated and
A2: A2,B are_weakly_separated;
    A2 \ B,B \ A2 are_separated by A2;
    then
A3: A2 \ B,(B \ A1) /\ (B \ A2) are_separated by Th40;
    A1 \ B,B \ A1 are_separated by A1;
    then A1 \ B,(B \ A1) /\ (B \ A2) are_separated by Th40;
    then (A1 \ B) \/ (A2 \ B),(B \ A1) /\ (B \ A2) are_separated by A3,Th41;
    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;
  end;
end;

::First Characterization of Weakly Separated Subsets of Topological Spaces.

theorem Th54:
  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) by XBOOLE_1:79;
  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;
    then consider C1, C2 being Subset of X such that
A2: B1 c= C1 & B2 c= C2 and
A3: C1 misses B2 and
A4: C2 misses B1 and
A5: C1 is closed & C2 is closed by Th42;
    C1 /\ B2 = {} by A3,XBOOLE_0:def 7;
    then C1 /\ A2 \ C1 /\ A1 = {} by XBOOLE_1:50;
    then
A6: C1 /\ A2 c= C1 /\ A1 by XBOOLE_1:37;
    take C1,C2;
    take C = (C1 \/ C2)`;
    B1 \/ B2 c= C1 \/ C2 by A2,XBOOLE_1:13;
    then C c= (B1 \/ B2)`by SUBSET_1:12;
    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:14;
    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
A7: C /\ (A1 \/ A2) c= {}X \/ (A1 /\ A2) /\ (A1 \/ A2) by A1,XBOOLE_0:def 7;
    C2 /\ B1 = {} by A4,XBOOLE_0:def 7;
    then C2 /\ A1 \ C2 /\ A2 = {} by XBOOLE_1:50;
    then
A8: C2 /\ A1 c= C2 /\ A2 by XBOOLE_1:37;
    C2 /\ (A1 \/ A2) = C2 /\ A1 \/ C2 /\ A2 by XBOOLE_1:23;
    then
A9: C2 /\ (A1 \/ A2) = C2 /\ A2 by A8,XBOOLE_1:12;
    C1 /\ (A1 \/ A2) = C1 /\ A1 \/ C1 /\ A2 by XBOOLE_1:23;
    then
A10: C1 /\ (A1 \/ A2) = C1 /\ A1 by A6,XBOOLE_1:12;
    [#]X = C \/ C` & (A1 /\ A2) /\ (A1 \/ A2) c= A1 /\ A2 by PRE_TOPC:2
,XBOOLE_1:17;
    hence thesis by A5,A10,A9,A7,XBOOLE_1:1,17;
  end;
  given C1, C2, C being Subset of X such that
A11: C1 /\ (A1 \/ A2) c= A1 and
A12: C2 /\ (A1 \/ A2) c= A2 and
A13: C /\ (A1 \/ A2) c= A1 /\ A2 and
A14: the carrier of X = (C1 \/ C2) \/ C and
A15: C1 is closed & C2 is closed and
  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
    (C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2)) c= A1 /\ A2 by A11,A12,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
A16: (C1 /\ C2) /\ (B1 \/ B2) = {} by XBOOLE_1:55;
    A1 /\ A2 c= A2 by XBOOLE_1:17;
    then C /\ (A1 \/ A2) c= A2 by A13,XBOOLE_1:1;
    then C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A12,XBOOLE_1:8;
    then
A17: (C2 \/ C) /\ (A1 \/ A2) c= A2 by XBOOLE_1:23;
    A1 c= A1 \/ A2 by XBOOLE_1:7;
    then B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by A17,XBOOLE_1:35;
    then
A18: B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
    A1 /\ A2 c= A1 by XBOOLE_1:17;
    then C /\ (A1 \/ A2) c= A1 by A13,XBOOLE_1:1;
    then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 by A11,XBOOLE_1:8;
    then
A19: (C \/ C1) /\ (A1 \/ A2) c= A1 by XBOOLE_1:23;
    A2 c= A1 \/ A2 by XBOOLE_1:7;
    then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) by A19,XBOOLE_1:35;
    then
A20: B2 c= (A1 \/ A2) \ (C \/ C1) by XBOOLE_1:47;
    take C1,C2;
A21: A1 \/ A2 c= [#]X;
    then A1 \/ A2 c= (C2 \/ C) \/ C1 by A14,XBOOLE_1:4;
    then
A22: (A1 \/ A2) \ (C2 \/ C) c= C1 by XBOOLE_1:43;
    A1 \/ A2 c= (C \/ C1) \/ C2 by A14,A21,XBOOLE_1:4;
    then (A1 \/ A2) \ (C \/ C1) c= C2 by XBOOLE_1:43;
    hence thesis by A15,A20,A18,A22,A16,XBOOLE_0:def 7,XBOOLE_1:1;
  end;
  then B1,B2 are_separated by Th43;
  hence thesis;
end;

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

theorem Th55:
  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 that
A1: A1,A2 are_weakly_separated and
A2: not A1 c= A2 and
A3: not A2 c= A1;
  set B1 = A1 \ A2, B2 = A2 \ A1;
A4: B1 <> {} by A2,XBOOLE_1:37;
A5: B2 <> {} by A3,XBOOLE_1:37;
A6: A1 c= A1 \/ A2 by XBOOLE_1:7;
A7: A2 c= A1 \/ A2 by XBOOLE_1:7;
  consider C1, C2, C being Subset of X such that
A8: C1 /\ (A1 \/ A2) c= A1 and
A9: C2 /\ (A1 \/ A2) c= A2 and
A10: C /\ (A1 \/ A2) c= A1 /\ A2 and
A11: the carrier of X = (C1 \/ C2) \/ C and
A12: C1 is closed & C2 is closed and
A13: C is open by A1,Th54;
  A1 /\ A2 c= A1 by XBOOLE_1:17;
  then C /\ (A1 \/ A2) c= A1 by A10,XBOOLE_1:1;
  then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 by A8,XBOOLE_1:8;
  then (C \/ C1) /\ (A1 \/ A2) c= A1 by XBOOLE_1:23;
  then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) by A7,XBOOLE_1:35;
  then
A14: B2 c= (A1 \/ A2) \ (C \/ C1) by XBOOLE_1:47;
  A1 /\ A2 c= A2 by XBOOLE_1:17;
  then C /\ (A1 \/ A2) c= A2 by A10,XBOOLE_1:1;
  then C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:8;
  then (C2 \/ C) /\ (A1 \/ A2) c= A2 by XBOOLE_1:23;
  then B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by A6,XBOOLE_1:35;
  then
A15: B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
A16: A1 \/ A2 c= [#]X;
  then A1 \/ A2 c= (C \/ C1) \/ C2 by A11,XBOOLE_1:4;
  then (A1 \/ A2) \ (C \/ C1) c= C2 by XBOOLE_1:43;
  then reconsider D2 = C2 as non empty Subset of X by A14,A5,XBOOLE_1:1,3;
  A1 \/ A2 c= (C2 \/ C) \/ C1 by A11,A16,XBOOLE_1:4;
  then (A1 \/ A2) \ (C2 \/ C) c= C1 by XBOOLE_1:43;
  then reconsider D1 = C1 as non empty Subset of X by A15,A4,XBOOLE_1:1,3;
  take D1,D2;
  now
    assume
A17: 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 A11,A17;
      take C0;
      thus thesis by A10,A11,A13;
    end;
  end;
  hence thesis by A8,A9,A12;
end;

theorem Th56:
  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;
  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
A2: 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 by Th54;
    take C1,C2,C;
    thus thesis by A1,A2,XBOOLE_1:28;
  end;
  given C1, C2, C being Subset of X such that
A3: A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
  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,A3,XBOOLE_1:28;
  end;
  hence thesis by Th54;
end;

theorem Th57:
  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 A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
  then consider C1, C2 being non empty Subset of X such that
A2: C1 is closed & C2 is closed & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/
  A2) c= A2 and
A3: 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
Th55;
  take C1,C2;
  now
    assume not A1 \/ A2 = C1 \/ C2;
    then consider C being non empty Subset of X such that
A4: C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1
    \/ C2) \/ C by A1,A3,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,A4,XBOOLE_1:28;
    end;
  end;
  hence thesis by A1,A2,XBOOLE_1:28;
end;

::Second Characterization of Weakly Separated Subsets of Topological Spaces.

theorem Th58:
  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) by XBOOLE_1:79;
  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;
    then consider C1, C2 being Subset of X such that
A2: B1 c= C1 & B2 c= C2 and
A3: C1 misses B2 and
A4: C2 misses B1 and
A5: C1 is open & C2 is open by Th44;
    C1 /\ B2 = {} by A3,XBOOLE_0:def 7;
    then C1 /\ A2 \ C1 /\ A1 = {} by XBOOLE_1:50;
    then
A6: C1 /\ A2 c= C1 /\ A1 by XBOOLE_1:37;
    take C1,C2;
    take C = (C1 \/ C2)`;
    B1 \/ B2 c= C1 \/ C2 by A2,XBOOLE_1:13;
    then C c= (B1 \/ B2)`by SUBSET_1:12;
    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:14;
    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
A7: C /\ (A1 \/ A2) c= {}X \/ (A1 /\ A2) /\ (A1 \/ A2) by A1,XBOOLE_0:def 7;
    C2 /\ B1 = {} by A4,XBOOLE_0:def 7;
    then C2 /\ A1 \ C2 /\ A2 = {} by XBOOLE_1:50;
    then
A8: C2 /\ A1 c= C2 /\ A2 by XBOOLE_1:37;
    C2 /\ (A1 \/ A2) = C2 /\ A1 \/ C2 /\ A2 by XBOOLE_1:23;
    then
A9: C2 /\ (A1 \/ A2) = C2 /\ A2 by A8,XBOOLE_1:12;
    C1 /\ (A1 \/ A2) = C1 /\ A1 \/ C1 /\ A2 by XBOOLE_1:23;
    then
A10: C1 /\ (A1 \/ A2) = C1 /\ A1 by A6,XBOOLE_1:12;
    [#]X = C` \/ C & (A1 /\ A2) /\ (A1 \/ A2) c= A1 /\ A2 by PRE_TOPC:2
,XBOOLE_1:17;
    hence thesis by A5,A10,A9,A7,XBOOLE_1:1,17;
  end;
  given C1, C2, C being Subset of X such that
A11: C1 /\ (A1 \/ A2) c= A1 and
A12: C2 /\ (A1 \/ A2) c= A2 and
A13: C /\ (A1 \/ A2) c= A1 /\ A2 and
A14: the carrier of X = (C1 \/ C2) \/ C and
A15: C1 is open & C2 is open and
  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
    (C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2)) c= A1 /\ A2 by A11,A12,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
A16: (C1 /\ C2) /\ (B1 \/ B2) = {} by XBOOLE_1:55;
    A1 /\ A2 c= A2 by XBOOLE_1:17;
    then C /\ (A1 \/ A2) c= A2 by A13,XBOOLE_1:1;
    then C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A12,XBOOLE_1:8;
    then
A17: (C2 \/ C) /\ (A1 \/ A2) c= A2 by XBOOLE_1:23;
    A1 c= A1 \/ A2 by XBOOLE_1:7;
    then B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by A17,XBOOLE_1:35;
    then
A18: B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
    A1 /\ A2 c= A1 by XBOOLE_1:17;
    then C /\ (A1 \/ A2) c= A1 by A13,XBOOLE_1:1;
    then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 by A11,XBOOLE_1:8;
    then
A19: (C \/ C1) /\ (A1 \/ A2) c= A1 by XBOOLE_1:23;
    A2 c= A1 \/ A2 by XBOOLE_1:7;
    then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) by A19,XBOOLE_1:35;
    then
A20: B2 c= (A1 \/ A2) \ (C \/ C1) by XBOOLE_1:47;
    take C1,C2;
A21: A1 \/ A2 c= [#]X;
    then A1 \/ A2 c= (C2 \/ C) \/ C1 by A14,XBOOLE_1:4;
    then
A22: (A1 \/ A2) \ (C2 \/ C) c= C1 by XBOOLE_1:43;
    A1 \/ A2 c= (C \/ C1) \/ C2 by A14,A21,XBOOLE_1:4;
    then (A1 \/ A2) \ (C \/ C1) c= C2 by XBOOLE_1:43;
    hence thesis by A15,A20,A18,A22,A16,XBOOLE_0:def 7,XBOOLE_1:1;
  end;
  then B1,B2 are_separated by Th45;
  hence thesis;
end;

theorem Th59:
  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 that
A1: A1,A2 are_weakly_separated and
A2: not A1 c= A2 and
A3: not A2 c= A1;
  set B1 = A1 \ A2, B2 = A2 \ A1;
A4: B1 <> {} by A2,XBOOLE_1:37;
A5: B2 <> {} by A3,XBOOLE_1:37;
A6: A1 c= A1 \/ A2 by XBOOLE_1:7;
A7: A2 c= A1 \/ A2 by XBOOLE_1:7;
  consider C1, C2, C being Subset of X such that
A8: C1 /\ (A1 \/ A2) c= A1 and
A9: C2 /\ (A1 \/ A2) c= A2 and
A10: C /\ (A1 \/ A2) c= A1 /\ A2 and
A11: the carrier of X = (C1 \/ C2) \/ C and
A12: C1 is open & C2 is open and
A13: C is closed by A1,Th58;
  A1 /\ A2 c= A1 by XBOOLE_1:17;
  then C /\ (A1 \/ A2) c= A1 by A10,XBOOLE_1:1;
  then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 by A8,XBOOLE_1:8;
  then (C \/ C1) /\ (A1 \/ A2) c= A1 by XBOOLE_1:23;
  then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) by A7,XBOOLE_1:35;
  then
A14: B2 c= (A1 \/ A2) \ (C \/ C1) by XBOOLE_1:47;
  A1 /\ A2 c= A2 by XBOOLE_1:17;
  then C /\ (A1 \/ A2) c= A2 by A10,XBOOLE_1:1;
  then C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:8;
  then (C2 \/ C) /\ (A1 \/ A2) c= A2 by XBOOLE_1:23;
  then B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by A6,XBOOLE_1:35;
  then
A15: B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
A16: A1 \/ A2 c= [#]X;
  then A1 \/ A2 c= (C \/ C1) \/ C2 by A11,XBOOLE_1:4;
  then (A1 \/ A2) \ (C \/ C1) c= C2 by XBOOLE_1:43;
  then reconsider D2 = C2 as non empty Subset of X by A14,A5,XBOOLE_1:1,3;
  A1 \/ A2 c= (C2 \/ C) \/ C1 by A11,A16,XBOOLE_1:4;
  then (A1 \/ A2) \ (C2 \/ C) c= C1 by XBOOLE_1:43;
  then reconsider D1 = C1 as non empty Subset of X by A15,A4,XBOOLE_1:1,3;
  take D1,D2;
  now
    assume
A17: 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 A11,A17;
      take C0;
      thus thesis by A10,A11,A13;
    end;
  end;
  hence thesis by A8,A9,A12;
end;

theorem Th60:
  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;
  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
A2: 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 by Th58;
    take C1,C2,C;
    thus thesis by A1,A2,XBOOLE_1:28;
  end;
  given C1, C2, C being Subset of X such that
A3: A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
  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,A3,XBOOLE_1:28;
  end;
  hence thesis by Th58;
end;

theorem Th61:
  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 A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
  then consider C1, C2 being non empty Subset of X such that
A2: C1 is open & C2 is open & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2)
  c= A2 and
A3: 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
Th59;
  take C1,C2;
  now
    assume not A1 \/ A2 = C1 \/ C2;
    then consider C being non empty Subset of X such that
A4: C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1
    \/ C2 ) \/ C by A1,A3,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,A4,XBOOLE_1:28;
    end;
  end;
  hence thesis by A1,A2,XBOOLE_1:28;
end;

::A Characterization of Separated Subsets by means of Weakly Separated ones.

theorem Th62:
  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 & B1 is open & B2
    is open by Th45;
    take B1,B2;
    thus thesis by A1,Th49;
  end;
  given B1, B2 being Subset of X such that
A2: B1,B2 are_weakly_separated and
A3: A1 c= B1 and
A4: A2 c= B2 and
A5: B1 /\ B2 misses A1 \/ A2;
  B1 /\ B2 misses A1 by A5,XBOOLE_1:7,63;
  then
A6: (B1 /\ B2) /\ A1 = {} by XBOOLE_0:def 7;
  B1 /\ B2 misses A2 by A5,XBOOLE_1:7,63;
  then
A7: (B1 /\ B2) /\ A2 = {} by XBOOLE_0:def 7;
  B1 /\ A2 c= A2 & B1 /\ A2 c= B1 /\ B2 by A4,XBOOLE_1:17,26;
  then
A8: B1 /\ A2 = {} by A7,XBOOLE_1:3,19;
  A2 \ B1 c= B2 \ B1 by A4,XBOOLE_1:33;
  then
A9: A2 \ B1 /\ A2 c= B2 \ B1 by XBOOLE_1:47;
  A1 /\ B2 c= A1 & A1 /\ B2 c= B1 /\ B2 by A3,XBOOLE_1:17,26;
  then
A10: A1 /\ B2 = {} by A6,XBOOLE_1:3,19;
  A1 \ B2 c= B1 \ B2 by A3,XBOOLE_1:33;
  then
A11: A1 \ A1 /\ B2 c= B1 \ B2 by XBOOLE_1:47;
  B1 \ B2,B2 \ B1 are_separated by A2;
  hence thesis by A10,A8,A11,A9,CONNSP_1:7;
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

  for A1, A2 being Subset of X st A1 =
  the carrier of X1 & A2 = the carrier of X2 holds A1,A2 are_separated;
  symmetry;
end;

notation
  let X be TopStruct;
  let X1, X2 be SubSpace of X;
  antonym X1,X2 are_not_separated for X1,X2 are_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 A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  assume X1,X2 are_separated;
  then A1,A2 are_separated;
  then A1 misses A2 by CONNSP_1:1;
  hence thesis;
end;

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;
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
A1: A1 is closed & A2 is closed by Th11;
  thus X1 misses X2 implies X1,X2 are_separated
  by A1,Th34;
  assume X1,X2 are_separated;
  then A1,A2 are_separated;
  then A1 misses A2 by CONNSP_1:1;
  hence thesis;
end;

theorem
  X = X1 union X2 & X1,X2 are_separated implies X1 is closed SubSpace of X
proof
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  assume X = X1 union X2;
  then
A1: A1 \/ A2 = [#]X by Def2;
  assume X1,X2 are_separated;
  then A1,A2 are_separated;
  then A1 is closed by A1,CONNSP_1:4;
  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
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  assume
A1: X1 union X2 is closed SubSpace of X;
  assume X1,X2 are_separated;
  then
A2: A1,A2 are_separated;
  A1 \/ A2 = the carrier of X1 union X2 by Def2;
  then A1 \/ A2 is closed by A1,Th11;
  then A1 is closed by A2,Th35;
  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;
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
A1: A1 is open & A2 is open by Th16;
  thus X1 misses X2 implies X1,X2 are_separated
  by A1,Th37;
  assume X1,X2 are_separated;
  then A1,A2 are_separated;
  then A1 misses A2 by CONNSP_1:1;
  hence thesis;
end;

theorem
  X = X1 union X2 & X1,X2 are_separated implies X1 is open SubSpace of X
proof
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  assume X = X1 union X2;
  then
A1: A1 \/ A2 = [#]X by Def2;
  assume X1,X2 are_separated;
  then A1,A2 are_separated;
  then A1 is open by A1,CONNSP_1:4;
  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
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  assume
A1: X1 union X2 is open SubSpace of X;
  assume X1,X2 are_separated;
  then
A2: A1,A2 are_separated;
  A1 \/ A2 = the carrier of X1 union X2 by Def2;
  then A1 \/ A2 is open by A1,Th16;
  then A1 is open by A2,Th38;
  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 and
A2: X2 meets Y;
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  reconsider C = the carrier of Y as Subset of X by Th1;
  assume X1,X2 are_separated;
  then
A3: A1,A2 are_separated;
  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,A2,Def4;
    hence D1,D2 are_separated by A3,Th39;
  end;
  hence X1 meet Y,X2 meet Y are_separated;
  then X1 meet Y,Y meet X2 are_separated by A2,Th26;
  hence Y meet X1,Y meet X2 are_separated by A1,Th26;
end;

theorem Th71:
  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
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  let Y1, Y2 be SubSpace of X such that
A1: Y1 is SubSpace of X1 & Y2 is SubSpace of X2;
  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
A3: B1 c= A1 & B2 c= A2 by A1,Th4;
    A1,A2 are_separated by A2;
    hence B1,B2 are_separated by A3,CONNSP_1:7;
  end;
  hence thesis;
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 Th27;
  Y is SubSpace of Y by Th2;
  hence thesis by A1,Th71;
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
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  let Y be non empty SubSpace of X;
  reconsider C = the carrier of Y as Subset of X by Th1;
A1: Y is SubSpace of Y by Th2;
  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
A2: A1,C are_separated & A2,C are_separated;
    now
      let D, C be Subset of X;
      assume that
A3:   D = the carrier of X1 union X2 and
A4:   C = the carrier of Y;
      A1 \/ A2 = D by A3,Def2;
      hence D,C are_separated by A2,A4,Th41;
    end;
    hence thesis;
  end;
  assume
A5: X1 union X2,Y are_separated;
  X1 is SubSpace of X1 union X2 & X2 is SubSpace of X1 union X2 by Th22;
  hence thesis by A5,A1,Th71;
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 A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 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;
    then consider C1, C2 being Subset of X such that
A1: A1 c= C1 and
A2: A2 c= C2 and
A3: C1 misses A2 & C2 misses A1 and
A4: C1 is closed and
A5: C2 is closed by Th42;
    C1 is non empty by A1,XBOOLE_1:3;
    then consider Y1 being strict closed non empty SubSpace of X such that
A6: C1 = the carrier of Y1 by A4,Th15;
    C2 is non empty by A2,XBOOLE_1:3;
    then consider Y2 being strict closed non empty SubSpace of X such that
A7: C2 = the carrier of Y2 by A5,Th15;
    take Y1,Y2;
    thus thesis by A1,A2,A3,A6,A7,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 & 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
      reconsider C2 = the carrier of Y2 as Subset of X by Th1;
      reconsider C1 = the carrier of Y1 as Subset of X by Th1;
      take C1,C2;
      thus thesis by A8,A9,Th4,Th11;
    end;
    hence A1,A2 are_separated by Th42;
  end;
  hence thesis;
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 A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 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;
    then consider C1, C2 being Subset of X such that
A1: A1 c= C1 and
A2: A2 c= C2 and
A3: C1 /\ C2 misses A1 \/ A2 and
A4: C1 is closed and
A5: C2 is closed by Th43;
    C1 is non empty by A1,XBOOLE_1:3;
    then consider Y1 being strict closed non empty SubSpace of X such that
A6: C1 = the carrier of Y1 by A4,Th15;
    C2 is non empty by A2,XBOOLE_1:3;
    then consider Y2 being strict closed non empty SubSpace of X such that
A7: C2 = the carrier of Y2 by A5,Th15;
    take Y1,Y2;
    now
      assume not Y1 misses Y2;
      then
A8:   the carrier of Y1 meet Y2 = C1 /\ C2 by A6,A7,Def4;
      the carrier of X1 union X2 = A1 \/ A2 by Def2;
      hence Y1 meet Y2 misses X1 union X2 by A3,A8;
    end;
    hence thesis by A1,A2,A6,A7,Th4;
  end;
  given Y1, Y2 being closed non empty SubSpace of X such that
A9: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A10: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
  now
    let A1, A2 be Subset of X such that
A11: 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
      reconsider C2 = the carrier of Y2 as Subset of X by Th1;
      reconsider C1 = the carrier of Y1 as Subset of X by Th1;
      take C1,C2;
      now
        per cases;
        suppose
          Y1 misses Y2;
          then C1 misses C2;
          then C1 /\ C2 = {} by XBOOLE_0:def 7;
          hence C1 /\ C2 misses A1 \/ A2 by XBOOLE_1:65;
        end;
        suppose
A12:      not Y1 misses Y2;
A13:      the carrier of X1 union X2 = A1 \/ A2 by A11,Def2;
          the carrier of Y1 meet Y2 = C1 /\ C2 by A12,Def4;
          hence C1 /\ C2 misses A1 \/ A2 by A10,A12,A13;
        end;
      end;
      hence thesis by A9,A11,Th4,Th11;
    end;
    hence A1,A2 are_separated by Th43;
  end;
  hence thesis;
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 A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 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;
    then consider C1 being Subset of X, C2 being Subset of X such that
A1: A1 c= C1 and
A2: A2 c= C2 and
A3: C1 misses A2 & C2 misses A1 and
A4: C1 is open and
A5: C2 is open by Th44;
    C1 is non empty by A1,XBOOLE_1:3;
    then consider Y1 being strict open non empty SubSpace of X such that
A6: C1 = the carrier of Y1 by A4,Th20;
    C2 is non empty by A2,XBOOLE_1:3;
    then consider Y2 being strict open non empty SubSpace of X such that
A7: C2 = the carrier of Y2 by A5,Th20;
    take Y1,Y2;
    thus thesis by A1,A2,A3,A6,A7,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 & 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
      reconsider C2 = the carrier of Y2 as Subset of X by Th1;
      reconsider C1 = the carrier of Y1 as Subset of X by Th1;
      take C1,C2;
      thus thesis by A8,A9,Th4,Th16;
    end;
    hence A1,A2 are_separated by Th44;
  end;
  hence thesis;
end;

::Second Characterization of Separated Subspaces of Topological Spaces.

theorem Th77:
  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 A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 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;
    then consider C1, C2 being Subset of X such that
A1: A1 c= C1 and
A2: A2 c= C2 and
A3: C1 /\ C2 misses A1 \/ A2 and
A4: C1 is open and
A5: C2 is open by Th45;
    C1 is non empty by A1,XBOOLE_1:3;
    then consider Y1 being strict open non empty SubSpace of X such that
A6: C1 = the carrier of Y1 by A4,Th20;
    C2 is non empty by A2,XBOOLE_1:3;
    then consider Y2 being strict open non empty SubSpace of X such that
A7: C2 = the carrier of Y2 by A5,Th20;
    take Y1,Y2;
    now
      assume not Y1 misses Y2;
      then
A8:   the carrier of Y1 meet Y2 = C1 /\ C2 by A6,A7,Def4;
      the carrier of X1 union X2 = A1 \/ A2 by Def2;
      hence Y1 meet Y2 misses X1 union X2 by A3,A8;
    end;
    hence thesis by A1,A2,A6,A7,Th4;
  end;
  given Y1, Y2 being open non empty SubSpace of X such that
A9: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A10: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
  now
    let A1, A2 be Subset of X such that
A11: 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
      reconsider C2 = the carrier of Y2 as Subset of X by Th1;
      reconsider C1 = the carrier of Y1 as Subset of X by Th1;
      take C1,C2;
      now
        per cases;
        suppose
          Y1 misses Y2;
          then C1 misses C2;
          then C1 /\ C2 = {} by XBOOLE_0:def 7;
          hence C1 /\ C2 misses A1 \/ A2 by XBOOLE_1:65;
        end;
        suppose
A12:      not Y1 misses Y2;
A13:      the carrier of X1 union X2 = A1 \/ A2 by A11,Def2;
          the carrier of Y1 meet Y2 = C1 /\ C2 by A12,Def4;
          hence C1 /\ C2 misses A1 \/ A2 by A10,A12,A13;
        end;
      end;
      hence thesis by A9,A11,Th4,Th16;
    end;
    hence A1,A2 are_separated by Th45;
  end;
  hence thesis;
end;

definition
  let X be TopStruct, X1, X2 be SubSpace of X;
  pred X1,X2 are_weakly_separated means

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

notation
  let X be TopStruct, X1, X2 be SubSpace of X;
  antonym X1,X2 are_not_weakly_separated for X1,X2 are_weakly_separated;
end;

reserve X1, X2 for non empty SubSpace of X;

::Properties of Weakly Separated Subspaces of Topological Spaces.

theorem Th78:
  X1 misses X2 & X1,X2 are_weakly_separated iff X1,X2 are_separated
proof
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  thus X1 misses X2 & X1,X2 are_weakly_separated implies X1,X2 are_separated
  by Th46;
  assume X1,X2 are_separated;
  then
A1: A1,A2 are_separated;
  then A1 misses A2 by Th46;
  hence X1 misses X2;
  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,Th46;
  hence thesis;
end;

theorem Th79:
  X1 is SubSpace of X2 implies X1,X2 are_weakly_separated
by Th47,Th4;

theorem Th80:
  for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated
proof
  let X1, X2 be closed SubSpace of X;
  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 Th48;
end;

theorem Th81:
  for X1, X2 being open SubSpace of X holds X1,X2 are_weakly_separated
proof
  let X1, X2 be open SubSpace of X;
  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 Th49;
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
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  let Y be non empty SubSpace of X;
  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;
  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,Th50;
  end;
  hence thesis;
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
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  let Y1, Y2 be non empty SubSpace of X such that
A1: Y1 is SubSpace of X2 & Y2 is SubSpace of X1;
  reconsider B2 = the carrier of Y2 as Subset of X by Th1;
  reconsider B1 = the carrier of Y1 as Subset of X by Th1;
  assume X1,X2 are_weakly_separated;
  then
A2: A1,A2 are_weakly_separated;
A3: B1 c= A2 & B2 c= A1 by A1,Th4;
A4: 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 A3,A2,Th51;
  end;
  hence X1 union Y1,X2 union Y2 are_weakly_separated;
  thus thesis by A4;
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 A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 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;
    now
      let D, C be Subset of X;
      assume that
A3:   D = the carrier of X1 meet X2 and
A4:   C = the carrier of Y;
      A1 /\ A2 = D by A1,A3,Def4;
      hence D,C are_weakly_separated by A2,A4,Th52;
    end;
    hence thesis;
  end;
  hence thesis;
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
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  let Y be non empty SubSpace of X;
  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;
    now
      let D, C be Subset of X;
      assume that
A2:   D = the carrier of X1 union X2 and
A3:   C = the carrier of Y;
      A1 \/ A2 = D by A2,Def2;
      hence D,C are_weakly_separated by A1,A3,Th53;
    end;
    hence thesis;
  end;
  hence thesis;
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 A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  assume
A1: X1 meets X2;
A2: now
    assume
A3: 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 that
A4:   not X1 is SubSpace of X2 and
A5:   not X2 is SubSpace of X1;
      consider Y1, Y2 being closed non empty SubSpace of X such that
A6:   Y1 meet (X1 union X2) is SubSpace of X1 and
A7:   Y2 meet (X1 union X2) is SubSpace of X2 and
A8:   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 A3,A4,A5;
      reconsider C2 = the carrier of Y2 as Subset of X by Th1;
      reconsider C1 = the carrier of Y1 as Subset of X by Th1;
A9:  the carrier of X1 union X2 = A1 \/ A2 by Def2;
A10:  the carrier of Y1 union Y2 = C1 \/ C2 by Def2;
      now
        assume Y1 misses (X1 union X2);
        then
A11:    C1 misses (A1 \/ A2) by A9;
A12:    now
          per cases;
          suppose
            X1 union X2 is SubSpace of Y1 union Y2;
            then A1 \/ A2 c= C1 \/ C2 by A9,A10,Th4;
            then
A13:        A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
              .= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
              .= {} \/ (C2 /\ (A1 \/ A2)) by A11,XBOOLE_0:def 7
              .= C2 /\ (A1 \/ A2);
            then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
            then Y2 meets (X1 union X2) by A9;
            then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A9
,Def4;
            hence A1 \/ A2 c= A2 by A7,A13,Th4;
          end;
          suppose
            not X1 union X2 is SubSpace of Y1 union Y2;
            then consider Y being open non empty SubSpace of X such that
A14:        the TopStruct of X = (Y1 union Y2) union Y and
A15:        Y meet (X1 union X2) is SubSpace of X1 meet X2 by A8;
            reconsider C = the carrier of Y as Subset of X by Th1;
            the carrier of X = (C1 \/ C2) \/ C by A10,A14,Def2;
            then
A16:        A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
              .= (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 A11,XBOOLE_0:def 7
              .= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A17:        now
              assume C /\ (A1 \/ A2) <> {};
              then C meets (A1 \/ A2) by XBOOLE_0:def 7;
              then Y meets (X1 union X2) by A9;
              then
A18:          the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A9,Def4;
              the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
              then
A19:          C /\ (A1 \/ A2) c= A1 /\ A2 by A15,A18,Th4;
A20:          A1 /\ A2 c= A2 by XBOOLE_1:17;
              then
A21:          C /\ (A1 \/ A2) c= A2 by A19,XBOOLE_1:1;
              now
                per cases;
                suppose
                  C2 /\ (A1 \/ A2) = {};
                  hence A1 \/ A2 c= A2 by A16,A19,A20,XBOOLE_1:1;
                end;
                suppose
                  C2 /\ (A1 \/ A2) <> {};
                  then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y2 meets (X1 union X2) by A9;
                  then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2
                  ) by A9,Def4;
                  then C2 /\ (A1 \/ A2) c= A2 by A7,Th4;
                  hence A1 \/ A2 c= A2 by A16,A21,XBOOLE_1:8;
                end;
              end;
              hence A1 \/ A2 c= A2;
            end;
            now
              assume C2 /\ (A1 \/ A2) <> {};
              then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
              then Y2 meets (X1 union X2) by A9;
              then
A22:          the carrier of Y2 meet (X1 union X2) = C2 /\ ( A1 \/ A2) by A9
,Def4;
              then
A23:          C2 /\ (A1 \/ A2) c= A2 by A7,Th4;
              now
                per cases;
                suppose
                  C /\ (A1 \/ A2) = {};
                  hence A1 \/ A2 c= A2 by A7,A16,A22,Th4;
                end;
                suppose
                  C /\ (A1 \/ A2) <> {};
                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y meets (X1 union X2) by A9;
                  then
A24:              the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
                  by A9,Def4;
                  the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
                  then C /\ (A1 \/ A2) c= A1 /\ A2 by A15,A24,Th4;
                  then A1 \/ A2 c= A2 \/ A1 /\ A2 by A16,A23,XBOOLE_1:13;
                  hence A1 \/ A2 c= A2 by XBOOLE_1:12,17;
                end;
              end;
              hence A1 \/ A2 c= A2;
            end;
            hence A1 \/ A2 c= A2 by A16,A17;
          end;
        end;
        A1 c= A1 \/ A2 by XBOOLE_1:7;
        then A1 c= A2 by A12,XBOOLE_1:1;
        hence contradiction by A4,Th4;
      end;
      then
      the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A9,Def4;
      then
A25:  C1 /\ (A1 \/ A2) c= A1 by A6,Th4;
      now
        assume not Y2 meets (X1 union X2);
        then
A26:    C2 misses (A1 \/ A2) by A9;
A27:    now
          per cases;
          suppose
            X1 union X2 is SubSpace of Y1 union Y2;
            then A1 \/ A2 c= C1 \/ C2 by A9,A10,Th4;
            then
A28:        A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
              .= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
              .= (C1 /\ (A1 \/ A2)) \/ {} by A26,XBOOLE_0:def 7
              .= C1 /\ (A1 \/ A2);
            then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
            then Y1 meets (X1 union X2) by A9;
            then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A9
,Def4;
            hence A1 \/ A2 c= A1 by A6,A28,Th4;
          end;
          suppose
            not X1 union X2 is SubSpace of Y1 union Y2;
            then consider Y being open non empty SubSpace of X such that
A29:        the TopStruct of X = (Y1 union Y2) union Y and
A30:        Y meet (X1 union X2) is SubSpace of X1 meet X2 by A8;
            reconsider C = the carrier of Y as Subset of X by Th1;
            the carrier of X = (C1 \/ C2) \/ C by A10,A29,Def2;
            then
A31:        A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
              .= (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 A26,XBOOLE_0:def 7
              .= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A32:        now
              assume C /\ (A1 \/ A2) <> {};
              then C meets (A1 \/ A2) by XBOOLE_0:def 7;
              then Y meets (X1 union X2) by A9;
              then
A33:          the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A9,Def4;
              the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
              then
A34:          C /\ (A1 \/ A2) c= A1 /\ A2 by A30,A33,Th4;
A35:          A1 /\ A2 c= A1 by XBOOLE_1:17;
              then
A36:          C /\ (A1 \/ A2) c= A1 by A34,XBOOLE_1:1;
              now
                per cases;
                suppose
                  C1 /\ (A1 \/ A2) = {};
                  hence A1 \/ A2 c= A1 by A31,A34,A35,XBOOLE_1:1;
                end;
                suppose
                  C1 /\ (A1 \/ A2) <> {};
                  then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y1 meets (X1 union X2) by A9;
                  then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2
                  ) by A9,Def4;
                  then C1 /\ (A1 \/ A2) c= A1 by A6,Th4;
                  hence A1 \/ A2 c= A1 by A31,A36,XBOOLE_1:8;
                end;
              end;
              hence A1 \/ A2 c= A1;
            end;
            now
              assume C1 /\ (A1 \/ A2) <> {};
              then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
              then Y1 meets (X1 union X2) by A9;
              then
A37:          the carrier of Y1 meet (X1 union X2) = C1 /\ ( A1 \/ A2)
              by A9,Def4;
              then
A38:          C1 /\ (A1 \/ A2) c= A1 by A6,Th4;
              now
                per cases;
                suppose
                  C /\ (A1 \/ A2) = {};
                  hence A1 \/ A2 c= A1 by A6,A31,A37,Th4;
                end;
                suppose
                  C /\ (A1 \/ A2) <> {};
                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y meets (X1 union X2) by A9;
                  then
A39:              the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
                  by A9,Def4;
                  the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
                  then C /\ (A1 \/ A2) c= A1 /\ A2 by A30,A39,Th4;
                  then A1 \/ A2 c= A1 \/ A1 /\ A2 by A31,A38,XBOOLE_1:13;
                  hence A1 \/ A2 c= A1 by XBOOLE_1:12,17;
                end;
              end;
              hence A1 \/ A2 c= A1;
            end;
            hence A1 \/ A2 c= A1 by A31,A32;
          end;
        end;
        A2 c= A1 \/ A2 by XBOOLE_1:7;
        then A2 c= A1 by A27,XBOOLE_1:1;
        hence contradiction by A5,Th4;
      end;
      then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A9,Def4;
      then
A40:  C2 /\ (A1 \/ A2) c= A2 by A7,Th4;
A41:  C1 is closed & C2 is closed by Th11;
      now
        per cases;
        suppose
A42:      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)`;
            C misses (A1 \/ A2) by A42,SUBSET_1:24;
            then C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
            hence thesis by A41,PRE_TOPC:2,XBOOLE_1:2;
          end;
        end;
        suppose
A43:      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
A44:        the TopStruct of X = (Y1 union Y2) union Y and
A45:        Y meet (X1 union X2) is SubSpace of X1 meet X2 by A8,A9,A10,A43
,Th4;
            reconsider C = the carrier of Y as Subset of X by Th1;
A46:        the carrier of X = (the carrier of Y1 union Y2) \/ C by A44,Def2
              .= (C1 \/ C2) \/ C by Def2;
            now
              assume not Y meets (X1 union X2);
              then
A47:          C misses (A1 \/ A2) by A9;
              the carrier of X = (C1 \/ C2) \/ C by A10,A44,Def2;
              then A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
                .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by
XBOOLE_1:23
                .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A47,XBOOLE_0:def 7
                .= (C1 \/ C2) /\ (A1 \/ A2);
              hence contradiction by A43,XBOOLE_1:17;
            end;
            then
A48:        the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A9,Def4;
A49:        C is open by Th16;
            the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
            then C /\ (A1 \/ A2) c= A1 /\ A2 by A45,A48,Th4;
            hence thesis by A49,A46;
          end;
        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 A41,A25,A40,Th54;
      hence X1,X2 are_weakly_separated;
    end;
    hence X1,X2 are_weakly_separated by Th79;
  end;
A50: X is SubSpace of X by Th2;
  now
    assume X1,X2 are_weakly_separated;
    then
A51: A1,A2 are_weakly_separated;
    now
      assume that
A52:  not X1 is SubSpace of X2 and
A53:  not X2 is SubSpace of X1;
A54:  not A2 c= A1 by A53,Th4;
A55:  not A1 c= A2 by A52,Th4;
      then consider C1, C2 being non empty Subset of X such that
A56:  C1 is closed and
A57:  C2 is closed and
A58:  C1 /\ (A1 \/ A2) c= A1 and
A59:  C2 /\ (A1 \/ A2) c= A2 and
A60:  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
A51,A54,Th55;
A61:  now
        assume C2 misses (A1 \/ A2);
        then
A62:    C2 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
        now
          per cases;
          suppose
A63:        A1 \/ A2 c= C1 \/ C2;
A64:        A2 c= A1 \/ A2 by XBOOLE_1:7;
            A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A63,XBOOLE_1:28
              .= (C1 /\ (A1 \/ A2)) \/ {} by A62,XBOOLE_1:23
              .= C1 /\ (A1 \/ A2);
            hence contradiction by A54,A58,A64,XBOOLE_1:1;
          end;
          suppose
            not A1 \/ A2 c= C1 \/ C2;
            then consider C being non empty Subset of X such that
            C is open and
A65:        C /\ (A1 \/ A2) c= A1 /\ A2 and
A66:        the carrier of X = (C1 \/ C2) \/ C by A60;
            A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A66,XBOOLE_1:28
              .= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
              .= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A62,XBOOLE_1:23
              .= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
            then A1 \/ A2 c= A1 \/ A1 /\ A2 by A58,A65,XBOOLE_1:13;
            then
A67:        A1 \/ A2 c= A1 by XBOOLE_1:12,17;
            A2 c= A1 \/ A2 by XBOOLE_1:7;
            hence contradiction by A54,A67,XBOOLE_1:1;
          end;
        end;
        hence contradiction;
      end;
A68:  now
        assume C1 misses (A1 \/ A2);
        then
A69:    C1 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
        now
          per cases;
          suppose
A70:        A1 \/ A2 c= C1 \/ C2;
A71:        A1 c= A1 \/ A2 by XBOOLE_1:7;
            A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A70,XBOOLE_1:28
              .= {} \/ (C2 /\ (A1 \/ A2)) by A69,XBOOLE_1:23
              .= C2 /\ (A1 \/ A2);
            hence contradiction by A55,A59,A71,XBOOLE_1:1;
          end;
          suppose
            not A1 \/ A2 c= C1 \/ C2;
            then consider C being non empty Subset of X such that
            C is open and
A72:        C /\ (A1 \/ A2) c= A1 /\ A2 and
A73:        the carrier of X = (C1 \/ C2) \/ C by A60;
            A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A73,XBOOLE_1:28
              .= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
              .= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A69,XBOOLE_1:23
              .= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
            then A1 \/ A2 c= A2 \/ A1 /\ A2 by A59,A72,XBOOLE_1:13;
            then
A74:        A1 \/ A2 c= A2 by XBOOLE_1:12,17;
            A1 c= A1 \/ A2 by XBOOLE_1:7;
            hence contradiction by A55,A74,XBOOLE_1:1;
          end;
        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 Y2 being strict closed non empty SubSpace of X such that
A75:    C2 = the carrier of Y2 by A57,Th15;
A76:    the carrier of X1 union X2 = A1 \/ A2 by Def2;
        then Y2 meets (X1 union X2) by A61,A75;
        then
A77:    the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A75,A76,Def4
;
        consider Y1 being strict closed non empty SubSpace of X such that
A78:    C1 = the carrier of Y1 by A56,Th15;
A79:    the carrier of Y1 union Y2 = C1 \/ C2 by A78,A75,Def2;
A80:    now
          assume
A81:      not X1 union X2 is SubSpace of Y1 union Y2;
          then consider C being non empty Subset of X such that
A82:      C is open and
A83:      C /\ (A1 \/ A2) c= A1 /\ A2 and
A84:      the carrier of X = (C1 \/ C2) \/ C by A60,A76,A79,Th4;
A85:      not A1 \/ A2 c= C1 \/ C2 by A76,A79,A81,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
A86:        C = the carrier of Y by A82,Th20;
            now
              assume C misses (A1 \/ A2);
              then
A87:          C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
              A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A84,XBOOLE_1:28
                .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A87,XBOOLE_1:23
                .= (C1 \/ C2) /\ (A1 \/ A2);
              hence contradiction by A85,XBOOLE_1:17;
            end;
            then Y meets (X1 union X2) by A76,A86;
            then
A88:        the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A76,A86
,Def4;
            take Y;
A89:        the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
            the carrier of X = (the carrier of Y1 union Y2) \/ C by A78,A75,A84
,Def2
              .= the carrier of (Y1 union Y2) union Y by A86,Def2;
            hence thesis by A50,A83,A88,A89,Th4,Th5;
          end;
        end;
        take Y1,Y2;
        Y1 meets (X1 union X2) by A68,A78,A76;
        then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A78,A76
,Def4;
        hence thesis by A58,A59,A77,A80,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;
  hence thesis by A2;
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
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  assume
A1: X = X1 union X2;
  then
A2: A1 \/ A2 = the carrier of X by Def2;
  assume
A3: X1 meets X2;
A4: now
    assume
A5: 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
A6:   Y1 is SubSpace of X1 & Y2 is SubSpace of X2 and
A7:   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 A5;
      reconsider C2 = the carrier of Y2 as Subset of X by Th1;
      reconsider C1 = the carrier of Y1 as Subset of X by Th1;
A8:   now
        per cases;
        suppose
A9:       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 A9,XBOOLE_1:2;
          end;
        end;
        suppose
A10:      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
A11:        X = (Y1 union Y2) union Y and
A12:        Y is SubSpace of X1 meet X2 by A2,A7,A10,Def2;
            reconsider C = the carrier of Y as Subset of X by Th1;
            A1 /\ A2 = the carrier of X1 meet X2 by A3,Def4;
            then
A13:        C c= A1 /\ A2 by A12,Th4;
A14:        C is open by Th16;
            A1 \/ A2 = (the carrier of Y1 union Y2) \/ C by A2,A11,Def2
              .= (C1 \/ C2) \/ C by Def2;
            hence thesis by A14,A13;
          end;
        end;
      end;
A15:  C1 is closed & C2 is closed by Th11;
      C1 c= A1 & C2 c= A2 by A6,Th4;
      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,A15,A8,Th56;
      hence X1,X2 are_weakly_separated;
    end;
    hence X1,X2 are_weakly_separated by Th79;
  end;
  now
    assume X1,X2 are_weakly_separated;
    then
A16: A1,A2 are_weakly_separated;
    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
A17:  C1 is closed and
A18:  C2 is closed and
A19:  C1 c= A1 & C2 c= A2 and
A20:  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,A16,Th57;
      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 Y2 being strict closed non empty SubSpace of X such that
A21:    C2 = the carrier of Y2 by A18,Th15;
        consider Y1 being strict closed non empty SubSpace of X such that
A22:    C1 = the carrier of Y1 by A17,Th15;
        take Y1,Y2;
        now
          assume X <> Y1 union Y2;
          then consider C being non empty Subset of X such that
A23:      A1 \/ A2 = (C1 \/ C2) \/ C and
A24:      C c= A1 /\ A2 and
A25:      C is open by A1,A2,A20,A22,A21,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
A26:        C c= the carrier of X1 meet X2 by A3,A24,Def4;
            consider Y being strict open non empty SubSpace of X such that
A27:        C = the carrier of Y by A25,Th20;
            take Y;
            the carrier of X = (the carrier of Y1 union Y2) \/ C by A2,A22,A21
,A23,Def2
              .= the carrier of (Y1 union Y2) union Y by A27,Def2;
            hence thesis by A1,A27,A26,Th4,Th5;
          end;
        end;
        hence thesis by A19,A22,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 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;
  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
    reconsider A2 = the carrier of X2 as Subset of X by Th1;
    reconsider A1 = the carrier of X1 as Subset of X by Th1;
    assume X1,X2 are_weakly_separated;
    then X1,X2 are_separated by A2,Th78;
    then
A3: A1,A2 are_separated;
    A1 \/ A2 = [#]X by A1,Def2;
    then A1 is closed & A2 is closed by A3,CONNSP_1:4;
    hence thesis by Th11;
  end;
  thus thesis by Th80;
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 A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  assume
A1: X1 meets X2;
A2: [#]X = the carrier of X;
A3: now
    assume
A4: 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 that
A5:   not X1 is SubSpace of X2 and
A6:   not X2 is SubSpace of X1;
      consider Y1, Y2 being open non empty SubSpace of X such that
A7:   Y1 meet (X1 union X2) is SubSpace of X1 and
A8:   Y2 meet (X1 union X2) is SubSpace of X2 and
A9:   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 A4,A5,A6;
      reconsider C2 = the carrier of Y2 as Subset of X by Th1;
      reconsider C1 = the carrier of Y1 as Subset of X by Th1;
A10:  the carrier of X1 union X2 = A1 \/ A2 by Def2;
A11:  the carrier of Y1 union Y2 = C1 \/ C2 by Def2;
      now
        assume Y1 misses (X1 union X2);
        then
A12:    C1 misses (A1 \/ A2) by A10;
A13:    now
          per cases;
          suppose
            X1 union X2 is SubSpace of Y1 union Y2;
            then A1 \/ A2 c= C1 \/ C2 by A10,A11,Th4;
            then
A14:        A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
              .= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
              .= {} \/ (C2 /\ (A1 \/ A2)) by A12,XBOOLE_0:def 7
              .= C2 /\ (A1 \/ A2);
            then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
            then Y2 meets (X1 union X2) by A10;
            then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A10
,Def4;
            hence A1 \/ A2 c= A2 by A8,A14,Th4;
          end;
          suppose
            not X1 union X2 is SubSpace of Y1 union Y2;
            then consider Y being closed non empty SubSpace of X such that
A15:        the TopStruct of X = (Y1 union Y2) union Y and
A16:        Y meet (X1 union X2) is SubSpace of X1 meet X2 by A9;
            reconsider C = the carrier of Y as Subset of X by Th1;
            the carrier of X = (C1 \/ C2) \/ C by A11,A15,Def2;
            then
A17:        A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
              .= (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 A12,XBOOLE_0:def 7
              .= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A18:        now
              assume C /\ (A1 \/ A2) <> {};
              then C meets (A1 \/ A2) by XBOOLE_0:def 7;
              then Y meets (X1 union X2) by A10;
              then
A19:          the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A10,Def4
;
              the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
              then
A20:          C /\ (A1 \/ A2) c= A1 /\ A2 by A16,A19,Th4;
A21:          A1 /\ A2 c= A2 by XBOOLE_1:17;
              then
A22:          C /\ (A1 \/ A2) c= A2 by A20,XBOOLE_1:1;
              now
                per cases;
                suppose
                  C2 /\ (A1 \/ A2) = {};
                  hence A1 \/ A2 c= A2 by A17,A20,A21,XBOOLE_1:1;
                end;
                suppose
                  C2 /\ (A1 \/ A2) <> {};
                  then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y2 meets (X1 union X2) by A10;
                  then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2
                  ) by A10,Def4;
                  then C2 /\ (A1 \/ A2) c= A2 by A8,Th4;
                  hence A1 \/ A2 c= A2 by A17,A22,XBOOLE_1:8;
                end;
              end;
              hence A1 \/ A2 c= A2;
            end;
            now
              assume C2 /\ (A1 \/ A2) <> {};
              then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
              then Y2 meets (X1 union X2) by A10;
              then
A23:          the carrier of Y2 meet (X1 union X2) = C2 /\ ( A1 \/ A2) by A10
,Def4;
              then
A24:          C2 /\ (A1 \/ A2) c= A2 by A8,Th4;
              now
                per cases;
                suppose
                  C /\ (A1 \/ A2) = {};
                  hence A1 \/ A2 c= A2 by A8,A17,A23,Th4;
                end;
                suppose
                  C /\ (A1 \/ A2) <> {};
                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y meets (X1 union X2) by A10;
                  then
A25:              the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
                  by A10,Def4;
                  the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
                  then C /\ (A1 \/ A2) c= A1 /\ A2 by A16,A25,Th4;
                  then A1 \/ A2 c= A2 \/ A1 /\ A2 by A17,A24,XBOOLE_1:13;
                  hence A1 \/ A2 c= A2 by XBOOLE_1:12,17;
                end;
              end;
              hence A1 \/ A2 c= A2;
            end;
            hence A1 \/ A2 c= A2 by A17,A18;
          end;
        end;
        A1 c= A1 \/ A2 by XBOOLE_1:7;
        then A1 c= A2 by A13,XBOOLE_1:1;
        hence contradiction by A5,Th4;
      end;
      then
      the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A10,Def4;
      then
A26:  C1 /\ (A1 \/ A2) c= A1 by A7,Th4;
      now
        assume not Y2 meets (X1 union X2);
        then
A27:    C2 misses (A1 \/ A2) by A10;
A28:    now
          per cases;
          suppose
            X1 union X2 is SubSpace of Y1 union Y2;
            then A1 \/ A2 c= C1 \/ C2 by A10,A11,Th4;
            then
A29:        A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
              .= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
              .= (C1 /\ (A1 \/ A2)) \/ {} by A27,XBOOLE_0:def 7
              .= C1 /\ (A1 \/ A2);
            then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
            then Y1 meets (X1 union X2) by A10;
            then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A10
,Def4;
            hence A1 \/ A2 c= A1 by A7,A29,Th4;
          end;
          suppose
            not X1 union X2 is SubSpace of Y1 union Y2;
            then consider Y being closed non empty SubSpace of X such that
A30:        the TopStruct of X = (Y1 union Y2) union Y and
A31:        Y meet (X1 union X2) is SubSpace of X1 meet X2 by A9;
            reconsider C = the carrier of Y as Subset of X by Th1;
            the carrier of X = (C1 \/ C2) \/ C by A11,A30,Def2;
            then
A32:        A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
              .= (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 A27,XBOOLE_0:def 7
              .= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A33:        now
              assume C /\ (A1 \/ A2) <> {};
              then C meets (A1 \/ A2) by XBOOLE_0:def 7;
              then Y meets (X1 union X2) by A10;
              then
A34:          the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A10,Def4
;
              the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
              then
A35:          C /\ (A1 \/ A2) c= A1 /\ A2 by A31,A34,Th4;
A36:          A1 /\ A2 c= A1 by XBOOLE_1:17;
              then
A37:          C /\ (A1 \/ A2) c= A1 by A35,XBOOLE_1:1;
              now
                per cases;
                suppose
                  C1 /\ (A1 \/ A2) = {};
                  hence A1 \/ A2 c= A1 by A32,A35,A36,XBOOLE_1:1;
                end;
                suppose
                  C1 /\ (A1 \/ A2) <> {};
                  then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y1 meets (X1 union X2) by A10;
                  then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2
                  ) by A10,Def4;
                  then C1 /\ (A1 \/ A2) c= A1 by A7,Th4;
                  hence A1 \/ A2 c= A1 by A32,A37,XBOOLE_1:8;
                end;
              end;
              hence A1 \/ A2 c= A1;
            end;
            now
              assume C1 /\ (A1 \/ A2) <> {};
              then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
              then Y1 meets (X1 union X2) by A10;
              then
A38:          the carrier of Y1 meet (X1 union X2) = C1 /\ ( A1 \/ A2)
              by A10,Def4;
              then
A39:          C1 /\ (A1 \/ A2) c= A1 by A7,Th4;
              now
                per cases;
                suppose
                  C /\ (A1 \/ A2) = {};
                  hence A1 \/ A2 c= A1 by A7,A32,A38,Th4;
                end;
                suppose
                  C /\ (A1 \/ A2) <> {};
                  then C meets (A1 \/ A2) by XBOOLE_0:def 7;
                  then Y meets (X1 union X2) by A10;
                  then
A40:              the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
                  by A10,Def4;
                  the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
                  then C /\ (A1 \/ A2) c= A1 /\ A2 by A31,A40,Th4;
                  then A1 \/ A2 c= A1 \/ A1 /\ A2 by A32,A39,XBOOLE_1:13;
                  hence A1 \/ A2 c= A1 by XBOOLE_1:12,17;
                end;
              end;
              hence A1 \/ A2 c= A1;
            end;
            hence A1 \/ A2 c= A1 by A32,A33;
          end;
        end;
        A2 c= A1 \/ A2 by XBOOLE_1:7;
        then A2 c= A1 by A28,XBOOLE_1:1;
        hence contradiction by A6,Th4;
      end;
      then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A10,Def4;
      then
A41:  C2 /\ (A1 \/ A2) c= A2 by A8,Th4;
A42:  C1 is open & C2 is open by Th16;
      now
        per cases;
        suppose
A43:      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)`;
            C misses (A1 \/ A2) by A43,SUBSET_1:24;
            then C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
            hence thesis by A2,A42,PRE_TOPC:2,XBOOLE_1:2;
          end;
        end;
        suppose
A44:      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
A45:        the TopStruct of X = (Y1 union Y2) union Y and
A46:        Y meet (X1 union X2) is SubSpace of X1 meet X2 by A9,A10,A11,A44
,Th4;
            reconsider C = the carrier of Y as Subset of X by Th1;
A47:        the carrier of X = (the carrier of Y1 union Y2) \/ C by A45,Def2
              .= (C1 \/ C2) \/ C by Def2;
            now
              assume not Y meets (X1 union X2);
              then
A48:          C misses (A1 \/ A2) by A10;
              the carrier of X = (C1 \/ C2) \/ C by A11,A45,Def2;
              then A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
                .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by
XBOOLE_1:23
                .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A48,XBOOLE_0:def 7
                .= (C1 \/ C2) /\ (A1 \/ A2);
              hence contradiction by A44,XBOOLE_1:17;
            end;
            then
A49:        the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A10,Def4;
A50:        C is closed by Th11;
            the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
            then C /\ (A1 \/ A2) c= A1 /\ A2 by A46,A49,Th4;
            hence thesis by A50,A47;
          end;
        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 A42,A26,A41,Th58;
      hence X1,X2 are_weakly_separated;
    end;
    hence X1,X2 are_weakly_separated by Th79;
  end;
A51: X is SubSpace of X by Th2;
  now
    assume X1,X2 are_weakly_separated;
    then
A52: A1,A2 are_weakly_separated;
    now
      assume that
A53:  not X1 is SubSpace of X2 and
A54:  not X2 is SubSpace of X1;
A55:  not A2 c= A1 by A54,Th4;
A56:  not A1 c= A2 by A53,Th4;
      then consider C1, C2 being non empty Subset of X such that
A57:  C1 is open and
A58:  C2 is open and
A59:  C1 /\ (A1 \/ A2) c= A1 and
A60:  C2 /\ (A1 \/ A2) c= A2 and
A61:  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 A52,A55,Th59;
A62:  now
        assume C2 misses (A1 \/ A2);
        then
A63:    C2 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
        now
          per cases;
          suppose
A64:        A1 \/ A2 c= C1 \/ C2;
A65:        A2 c= A1 \/ A2 by XBOOLE_1:7;
            A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A64,XBOOLE_1:28
              .= (C1 /\ (A1 \/ A2)) \/ {} by A63,XBOOLE_1:23
              .= C1 /\ (A1 \/ A2);
            hence contradiction by A55,A59,A65,XBOOLE_1:1;
          end;
          suppose
            not A1 \/ A2 c= C1 \/ C2;
            then consider C being non empty Subset of X such that
            C is closed and
A66:        C /\ (A1 \/ A2) c= A1 /\ A2 and
A67:        the carrier of X = (C1 \/ C2) \/ C by A61;
            A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A67,XBOOLE_1:28
              .= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
              .= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A63,XBOOLE_1:23
              .= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
            then A1 \/ A2 c= A1 \/ A1 /\ A2 by A59,A66,XBOOLE_1:13;
            then
A68:        A1 \/ A2 c= A1 by XBOOLE_1:12,17;
            A2 c= A1 \/ A2 by XBOOLE_1:7;
            hence contradiction by A55,A68,XBOOLE_1:1;
          end;
        end;
        hence contradiction;
      end;
A69:  now
        assume C1 misses (A1 \/ A2);
        then
A70:    C1 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
        now
          per cases;
          suppose
A71:        A1 \/ A2 c= C1 \/ C2;
A72:        A1 c= A1 \/ A2 by XBOOLE_1:7;
            A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A71,XBOOLE_1:28
              .= {} \/ (C2 /\ (A1 \/ A2)) by A70,XBOOLE_1:23
              .= C2 /\ (A1 \/ A2);
            hence contradiction by A56,A60,A72,XBOOLE_1:1;
          end;
          suppose
            not A1 \/ A2 c= C1 \/ C2;
            then consider C being non empty Subset of X such that
            C is closed and
A73:        C /\ (A1 \/ A2) c= A1 /\ A2 and
A74:        the carrier of X = (C1 \/ C2) \/ C by A61;
            A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A74,XBOOLE_1:28
              .= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
              .= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A70,XBOOLE_1:23
              .= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
            then A1 \/ A2 c= A2 \/ A1 /\ A2 by A60,A73,XBOOLE_1:13;
            then
A75:        A1 \/ A2 c= A2 by XBOOLE_1:12,17;
            A1 c= A1 \/ A2 by XBOOLE_1:7;
            hence contradiction by A56,A75,XBOOLE_1:1;
          end;
        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 Y2 being strict open non empty SubSpace of X such that
A76:    C2 = the carrier of Y2 by A58,Th20;
A77:    the carrier of X1 union X2 = A1 \/ A2 by Def2;
        then Y2 meets (X1 union X2) by A62,A76;
        then
A78:    the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A76,A77,Def4
;
        consider Y1 being strict open non empty SubSpace of X such that
A79:    C1 = the carrier of Y1 by A57,Th20;
A80:    the carrier of Y1 union Y2 = C1 \/ C2 by A79,A76,Def2;
A81:    now
          assume
A82:      not X1 union X2 is SubSpace of Y1 union Y2;
          then consider C being non empty Subset of X such that
A83:      C is closed and
A84:      C /\ (A1 \/ A2) c= A1 /\ A2 and
A85:      the carrier of X = (C1 \/ C2) \/ C by A61,A77,A80,Th4;
A86:      not A1 \/ A2 c= C1 \/ C2 by A77,A80,A82,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
A87:        C = the carrier of Y by A83,Th15;
            now
              assume C misses (A1 \/ A2);
              then
A88:          C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
              A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A85,XBOOLE_1:28
                .= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A88,XBOOLE_1:23
                .= (C1 \/ C2) /\ (A1 \/ A2);
              hence contradiction by A86,XBOOLE_1:17;
            end;
            then Y meets (X1 union X2) by A77,A87;
            then
A89:        the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A77,A87
,Def4;
            take Y;
A90:        the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
            the carrier of X = (the carrier of Y1 union Y2) \/ C by A79,A76,A85
,Def2
              .= the carrier of (Y1 union Y2) union Y by A87,Def2;
            hence thesis by A51,A84,A89,A90,Th4,Th5;
          end;
        end;
        take Y1,Y2;
        Y1 meets (X1 union X2) by A69,A79,A77;
        then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A79,A77
,Def4;
        hence thesis by A59,A60,A78,A81,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;
  hence thesis by A3;
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
  reconsider A2 = the carrier of X2 as Subset of X by Th1;
  reconsider A1 = the carrier of X1 as Subset of X by Th1;
  assume
A1: X = X1 union X2;
  then
A2: A1 \/ A2 = the carrier of X by Def2;
  assume
A3: X1 meets X2;
A4: now
    assume
A5: 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
A6:   Y1 is SubSpace of X1 & Y2 is SubSpace of X2 and
A7:   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 A5;
      reconsider C2 = the carrier of Y2 as Subset of X by Th1;
      reconsider C1 = the carrier of Y1 as Subset of X by Th1;
A8:   now
        per cases;
        suppose
A9:       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 A9,XBOOLE_1:2;
          end;
        end;
        suppose
A10:      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
A11:        X = (Y1 union Y2) union Y and
A12:        Y is SubSpace of X1 meet X2 by A2,A7,A10,Def2;
            reconsider C = the carrier of Y as Subset of X by Th1;
            A1 /\ A2 = the carrier of X1 meet X2 by A3,Def4;
            then
A13:        C c= A1 /\ A2 by A12,Th4;
A14:        C is closed by Th11;
            A1 \/ A2 = (the carrier of Y1 union Y2) \/ C by A2,A11,Def2
              .= (C1 \/ C2) \/ C by Def2;
            hence thesis by A14,A13;
          end;
        end;
      end;
A15:  C1 is open & C2 is open by Th16;
      C1 c= A1 & C2 c= A2 by A6,Th4;
      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,A15,A8,Th60;
      hence X1,X2 are_weakly_separated;
    end;
    hence X1,X2 are_weakly_separated by Th79;
  end;
  now
    assume X1,X2 are_weakly_separated;
    then
A16: A1,A2 are_weakly_separated;
    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
A17:  C1 is open and
A18:  C2 is open and
A19:  C1 c= A1 & C2 c= A2 and
A20:  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,A16,Th61;
      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 Y2 being strict open non empty SubSpace of X such that
A21:    C2 = the carrier of Y2 by A18,Th20;
        consider Y1 being strict open non empty SubSpace of X such that
A22:    C1 = the carrier of Y1 by A17,Th20;
        take Y1,Y2;
        now
          assume X <> Y1 union Y2;
          then consider C being non empty Subset of X such that
A23:      A1 \/ A2 = (C1 \/ C2) \/ C and
A24:      C c= A1 /\ A2 and
A25:      C is closed by A1,A2,A20,A22,A21,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
A26:        C c= the carrier of X1 meet X2 by A3,A24,Def4;
            consider Y being strict closed non empty SubSpace of X such that
A27:        C = the carrier of Y by A25,Th15;
            take Y;
            the carrier of X = (the carrier of Y1 union Y2) \/ C by A2,A22,A21
,A23,Def2
              .= the carrier of (Y1 union Y2) union Y by A27,Def2;
            hence thesis by A1,A27,A26,Th4,Th5;
          end;
        end;
        hence thesis by A19,A22,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 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;
  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
    reconsider A2 = the carrier of X2 as Subset of X by Th1;
    reconsider A1 = the carrier of X1 as Subset of X by Th1;
    assume X1,X2 are_weakly_separated;
    then X1,X2 are_separated by A2,Th78;
    then
A3: A1,A2 are_separated;
    A1 \/ A2 = [#]X by A1,Def2;
    then A1 is open & A2 is open by A3,CONNSP_1:4;
    hence thesis by Th16;
  end;
  thus thesis by Th81;
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 &( Y1 misses Y2 or Y1
    meet Y2 misses X1 union X2) by Th77;
    take Y1,Y2;
    thus thesis by A1,Th81;
  end;
  given Y1, Y2 being non empty SubSpace of X such that
A2: Y1,Y2 are_weakly_separated and
A3: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A4: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
  reconsider C2 = the carrier of Y2 as Subset of X by Th1;
  reconsider C1 = the carrier of Y1 as Subset of X by Th1;
  now
    let A1, A2 be Subset of X such that
A5: A1 = the carrier of X1 & A2 = the carrier of X2;
    now
      per cases;
      suppose
        Y1 misses Y2;
        then Y1,Y2 are_separated by A2,Th78;
        then
A6:     C1,C2 are_separated;
        A1 c= C1 & A2 c= C2 by A3,A5,Th4;
        hence A1,A2 are_separated by A6,CONNSP_1:7;
      end;
      suppose
A7:     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 A5,A7,Def2,Def4;
          hence thesis by A2,A3,A4,A5,A7,Th4;
        end;
        hence A1,A2 are_separated by Th62;
      end;
    end;
    hence A1,A2 are_separated;
  end;
  hence thesis;
end;

theorem :: WAYBEL34:30, AK, 20.02.2006
  for T being TopStruct holds T|[#]T = the TopStruct of T
proof
  let T be TopStruct;
  the TopStruct of T is strict SubSpace of T & the carrier of T = [#]the
  TopStruct of T by Th2,PRE_TOPC:10;
  hence thesis by PRE_TOPC:def 5;
end;