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

environ

 vocabularies XBOOLE_0, PRE_TOPC, SUBSET_1, STRUCT_0, TARSKI, TOPS_1, RCOMP_1,
      TSEP_1, CONNSP_1, SETFAM_1, TSEP_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, PRE_TOPC, STRUCT_0, TOPS_1, BORSUK_1,
      CONNSP_1, TSEP_1;
 constructors TOPS_1, CONNSP_1, BORSUK_1, TSEP_1;
 registrations STRUCT_0, PRE_TOPC;
 requirements BOOLE, SUBSET;
 definitions BORSUK_1, TSEP_1, XBOOLE_0, SUBSET_1, STRUCT_0;
 theorems PRE_TOPC, TOPS_1, CONNSP_1, BORSUK_1, TSEP_1, TDLAT_1, TDLAT_3,
      SUBSET_1, XBOOLE_0, XBOOLE_1;

begin :: 1. Certain Set-Decompositions of a Topological Space.

reserve X for non empty 1-sorted;

theorem Th1:
  for A, B being Subset of X holds ( A`) \ B` = B \ A
proof
  let A, B be Subset of X;
  A` \ B` = [#]X \ (A \/ B`) by XBOOLE_1:41;
  then A` \ B` = ( A`) /\ B`` by XBOOLE_1:53;
  hence thesis by SUBSET_1:13;
end;

:: Complemented Subsets.

definition
  let X be 1-sorted, A1, A2 be Subset of X;
  pred A1,A2 constitute_a_decomposition means
  :Def1:
  A1 misses A2 & A1 \/ A2 = the carrier of X;
  symmetry;
end;

notation
  let X be 1-sorted, A1, A2 be Subset of X;
  antonym A1,A2 do_not_constitute_a_decomposition for A1,A2
  constitute_a_decomposition;
end;

reserve A, A1, A2, B1, B2 for Subset of X;

theorem
  A1,A2 constitute_a_decomposition iff A1 misses A2 & A1 \/ A2 = [#]X by Def1;

theorem Th3:
  A1,A2 constitute_a_decomposition implies A1 = A2` & A2 = A1`
proof
  assume
A1: A1,A2 constitute_a_decomposition;
  then
A2: A1 misses A2 by Def1;
  then
A3: A1 c= A2` by SUBSET_1:23;
A4: A2 c= A1` by A2,SUBSET_1:23;
A5: A1 \/ A2 = [#]X by A1,Def1;
  then A2` c= A1 by TDLAT_1:1;
  hence A1 = A2` by A3,XBOOLE_0:def 10;
  A1` c= A2 by A5,TDLAT_1:1;
  hence thesis by A4,XBOOLE_0:def 10;
end;

theorem Th4:
  A1 = A2` or A2 = A1` implies A1,A2 constitute_a_decomposition
proof
  assume A1 = A2` or A2 = A1`;
  then A1 misses A2 & A1 \/ A2 = [#]X by TDLAT_1:1,SUBSET_1:23;
  hence thesis by Def1;
end;

theorem Th5:
  A, A` constitute_a_decomposition
proof
  A misses A` & A \/ A` = [#]X by PRE_TOPC:2,XBOOLE_1:79;
  hence A, A` constitute_a_decomposition by Def1;
end;

theorem
  {}X,[#]X constitute_a_decomposition
proof
  [#]X = ({}X)`;
  hence {}X,[#]X constitute_a_decomposition by Th5;
end;

theorem Th7:
  A,A do_not_constitute_a_decomposition
proof
  assume
A1: A,A constitute_a_decomposition;
  per cases;
  suppose
A2: A is non empty;
    A = A` by A1,Th3;
    then A misses A by SUBSET_1:23;
    then A /\ A = {} by XBOOLE_0:def 7;
    hence contradiction by A2;
  end;
  suppose
    A is empty;
    then {} = A \/ A .= the carrier of X by A1,Def1;
    hence contradiction;
  end;
end;

definition
  let X be non empty 1-sorted, A1, A2 be Subset of X;
  redefine pred A1,A2 constitute_a_decomposition;
  irreflexivity by Th7;
end;

theorem Th8:
  A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition
  implies A1 = A2
proof
  assume A1,A constitute_a_decomposition;
  then
A1: A1 = A` by Th3;
  assume A,A2 constitute_a_decomposition;
  hence thesis by A1,Th3;
end;

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

theorem Th9:
  A1,A2 constitute_a_decomposition implies (Cl A1),(Int A2)
  constitute_a_decomposition & (Int A1),(Cl A2) constitute_a_decomposition
proof
  assume
A1: A1,A2 constitute_a_decomposition;
  Cl A1 = (Int A1`)` by TDLAT_3:1;
  then Cl A1 = (Int A2)` by A1,Th3;
  hence (Cl A1),(Int A2) constitute_a_decomposition by Th4;
  Int A1 = (Cl A1`)` by TOPS_1:def 1;
  then Int A1 = (Cl A2)` by A1,Th3;
  hence (Int A1),(Cl A2) constitute_a_decomposition by Th4;
end;

theorem
  (Cl A),(Int A`) constitute_a_decomposition & 
  (Cl A`),(Int A) constitute_a_decomposition & 
  (Int A),(Cl A`) constitute_a_decomposition & 
  (Int A`),(Cl A) constitute_a_decomposition
proof
A1: A, A` constitute_a_decomposition by Th5;
  hence (Cl A),(Int A`) constitute_a_decomposition by Th9;
A2: A`,A constitute_a_decomposition by Th5;
  hence (Cl A`),(Int A) constitute_a_decomposition by Th9;
  thus (Int A),(Cl A`) constitute_a_decomposition by A2,Th9;
  thus thesis by A1,Th9;
end;

theorem Th11:
  for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition
  holds (A1 is open iff A2 is closed)
proof
  let A1, A2 be Subset of X;
  assume
A1: A1,A2 constitute_a_decomposition;
  then A2 = A1` by Th3;
  hence A1 is open implies A2 is closed by TOPS_1:4;
  assume
A2: A2 is closed;
  A1 = A2` by A1,Th3;
  hence thesis by A2,TOPS_1:3;
end;

theorem
  for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
  (A1 is closed iff A2 is open) by Th11;

reserve X for non empty 1-sorted;
reserve A, A1, A2, B1, B2 for Subset of X;

theorem Th13:
  A1,A2 constitute_a_decomposition & B1,B2
  constitute_a_decomposition implies (A1 /\ B1),(A2 \/ B2)
  constitute_a_decomposition
proof
  assume
A1: A1,A2 constitute_a_decomposition;
  then A1 misses A2 by Def1;
  then
A2: A1 /\ A2 = {} by XBOOLE_0:def 7;
  assume
A3: B1,B2 constitute_a_decomposition;
  then
A4: B1 \/ B2 = [#]X by Def1;
  B1 misses B2 by A3,Def1;
  then
A5: B1 /\ B2 = {}X by XBOOLE_0:def 7;
  (A1 /\ B1) /\ (A2 \/ B2) =((B1 /\ A1) /\ A2) \/ ((A1 /\ B1) /\ B2) by
XBOOLE_1:23
    .= (B1 /\ (A1 /\ A2)) \/ ((A1 /\ B1) /\ B2) by XBOOLE_1:16
    .= (B1 /\ (A1 /\ A2)) \/ (A1 /\ (B1 /\ B2)) by XBOOLE_1:16
    .= {}X by A5,A2;
  then
A6: (A1 /\ B1) misses (A2 \/ B2) by XBOOLE_0:def 7;
  (A1 /\ B1) \/ (A2 \/ B2) = (A1 \/ (A2 \/ B2)) /\ (B1 \/ (A2 \/ B2)) by
XBOOLE_1:24
    .= ((A1 \/ A2) \/ B2) /\ (B1 \/ (B2 \/ A2)) by XBOOLE_1:4
    .= ((A1 \/ A2) \/ B2) /\ ((B1 \/ B2) \/ A2) by XBOOLE_1:4
    .= ([#]X \/ B2) /\ ([#]X \/ A2) by A1,A4,Def1
    .= ([#]X \/ B2) /\ [#]X by XBOOLE_1:12
    .= [#]X /\ [#]X by XBOOLE_1:12
    .= [#]X;
  hence thesis by A6,Def1;
end;

theorem
  A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition
  implies (A1 \/ B1),(A2 /\ B2) constitute_a_decomposition by Th13;

begin

:: 2. A Duality Between Pairs of Weakly Separated Subsets.

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

theorem Th15:
  for A1, A2, C1, C2 being Subset of X st A1,C1
  constitute_a_decomposition & A2,C2 constitute_a_decomposition holds A1,A2
  are_weakly_separated iff C1,C2 are_weakly_separated
proof
  let A1, A2, C1, C2 be Subset of X;
  assume A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition;
  then
A1: C1 = A1` & C2 = A2` by Th3;
  thus A1,A2 are_weakly_separated implies C1,C2 are_weakly_separated
  proof
    assume A1 \ A2,A2 \ A1 are_separated;
    then C2 \ C1, C2` \ C1` are_separated by A1,Th1;
    then C2 \ C1,C1 \ C2 are_separated by Th1;
    hence thesis by TSEP_1:def 5;
  end;
  assume C1,C2 are_weakly_separated;
  then C1 \ C2,C2 \ C1 are_separated by TSEP_1:def 5;
  then C2` \ C1`,C2 \ C1 are_separated by Th1;
  then A2 \ A1,A1 \ A2 are_separated by A1,Th1;
  hence thesis by TSEP_1:def 5;
end;

theorem
  A1,A2 are_weakly_separated iff A1`, A2` are_weakly_separated
proof
  A1, A1` constitute_a_decomposition & A2, A2` constitute_a_decomposition
  by Th5;
  hence thesis by Th15;
end;

theorem
  for A1, A2, C1, C2 being Subset of X st A1,C1
  constitute_a_decomposition & A2,C2 constitute_a_decomposition holds A1,A2
  are_separated implies C1,C2 are_weakly_separated
proof
  let A1, A2, C1, C2 be Subset of X;
  assume
A1: A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition;
  assume A1,A2 are_separated;
  then A1,A2 are_weakly_separated by TSEP_1:46;
  hence thesis by A1,Th15;
end;

theorem Th18:
  for A1, A2, C1, C2 being Subset of X st A1,C1
  constitute_a_decomposition & A2,C2 constitute_a_decomposition holds A1 misses
  A2 & C1,C2 are_weakly_separated implies A1,A2 are_separated
proof
  let A1, A2, C1, C2 be Subset of X;
  assume
A1: A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition;
  assume
A2: A1 /\ A2 = {};
  assume C1,C2 are_weakly_separated;
  then
A3: A1,A2 are_weakly_separated by A1,Th15;
  A1 misses A2 by A2,XBOOLE_0:def 7;
  hence thesis by A3,TSEP_1:46;
end;

theorem
  for A1, A2, C1, C2 being Subset of X st A1,C1
constitute_a_decomposition & A2,C2 constitute_a_decomposition holds C1 \/ C2 =
  the carrier of X & C1,C2 are_weakly_separated implies A1,A2 are_separated
proof
  let A1, A2, C1, C2 be Subset of X;
  assume
A1: A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition;
  assume C1 \/ C2 = the carrier of X;
  then
A2: (C1 \/ C2)` = {}X by XBOOLE_1:37;
  A1 = C1` & A2 = C2` by A1,Th3;
  then A1 /\ A2 = {} by A2,XBOOLE_1:53;
  then
A3: A1 misses A2 by XBOOLE_0:def 7;
  assume C1,C2 are_weakly_separated;
  hence thesis by A1,A3,Th18;
end;

theorem
  A1,A2 constitute_a_decomposition implies (A1,A2 are_weakly_separated
  iff A1,A2 are_separated)
proof
  assume A1,A2 constitute_a_decomposition;
  then A1 misses A2 by Def1;
  hence thesis by TSEP_1:46;
end;

theorem Th21:
  A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated
proof
A1: (A1 \/ A2) \ A1 = A2 \ A1 & (A1 \/ A2) \ A2 = A1 \ A2 by XBOOLE_1:40;
  thus A1,A2 are_weakly_separated implies (A1 \/ A2) \ A1,(A1 \/ A2) \ A2
  are_separated
  proof
    assume A1 \ A2,A2 \ A1 are_separated;
    hence thesis by A1;
  end;
  assume (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated;
  hence thesis by A1,TSEP_1:def 5;
end;

::An Enlargement Theorem for Subsets.

theorem Th22:
  for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1
  \/ C2 = A1 \/ A2 holds C1,C2 are_weakly_separated implies A1,A2
  are_weakly_separated
proof
  let A1, A2, C1, C2 be Subset of X;
  assume C1 c= A1 & C2 c= A2;
  then
A1: (A1 \/ A2) \ A1 c= (A1 \/ A2) \ C1 & (A1 \/ A2) \ A2 c= (A1 \/ A2) \ C2
  by XBOOLE_1:34;
  assume
A2: C1 \/ C2 = A1 \/ A2;
  assume C1,C2 are_weakly_separated;
  then (A1 \/ A2) \ C1,(A1 \/ A2) \ C2 are_separated by A2,Th21;
  then (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated by A1,CONNSP_1:7;
  hence thesis by Th21;
end;

theorem Th23:
  A1,A2 are_weakly_separated iff A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated
proof
A1: A2 \ (A1 /\ A2) = A2 \ A1 by XBOOLE_1:47;
A2: A1 \ (A1 /\ A2) = A1 \ A2 by XBOOLE_1:47;
  thus A1,A2 are_weakly_separated implies A1 \ (A1 /\ A2),A2 \ (A1 /\ A2)
  are_separated
  proof
    assume A1 \ A2,A2 \ A1 are_separated;
    hence thesis by A2,XBOOLE_1:47;
  end;
  assume A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated;
  hence thesis by A2,A1,TSEP_1:def 5;
end;

::An Extenuation Theorem for Subsets.

theorem Th24:
  for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1
  /\ C2 = A1 /\ A2 holds A1,A2 are_weakly_separated implies C1,C2
  are_weakly_separated
proof
  let A1, A2, C1, C2 be Subset of X;
  assume C1 c= A1 & C2 c= A2;
  then
A1: C1 \ (C1 /\ C2) c= A1 \ (C1 /\ C2) & C2 \ (C1 /\ C2) c= A2 \ (C1 /\ C2)
  by XBOOLE_1:33;
  assume
A2: C1 /\ C2 = A1 /\ A2;
  assume A1,A2 are_weakly_separated;
  then A1 \ (C1 /\ C2),A2 \ (C1 /\ C2) are_separated by A2,Th23;
  then C1 \ (C1 /\ C2),C2 \ (C1 /\ C2) are_separated by A1,CONNSP_1:7;
  hence thesis by Th23;
end;

::Separated and Weakly Separated Subsets in Subspaces.

reserve X0 for non empty SubSpace of X,
  B1, B2 for Subset of X0;

theorem Th25:
  B1 = A1 & B2 = A2 implies (A1,A2 are_separated iff B1,B2 are_separated)
proof
  assume that
A1: B1 = A1 and
A2: B2 = A2;
A3: Cl B2 = (Cl A2) /\ [#]X0 by A2,PRE_TOPC:17;
A4: Cl B1 = (Cl A1) /\ [#]X0 by A1,PRE_TOPC:17;
  thus A1,A2 are_separated implies B1,B2 are_separated
  proof
    assume
A5: A1,A2 are_separated;
    then A1 misses Cl A2 by CONNSP_1:def 1;
    then A1 /\ Cl A2 = {} by XBOOLE_0:def 7;
    then B1 /\ Cl B2 = {} /\ [#]X0 by A1,A3,XBOOLE_1:16;
    then
A6: B1 misses Cl B2 by XBOOLE_0:def 7;
    Cl A1 misses A2 by A5,CONNSP_1:def 1;
    then Cl A1 /\ A2 = {} by XBOOLE_0:def 7;
    then Cl B1 /\ B2 = {} /\ [#]X0 by A2,A4,XBOOLE_1:16;
    then Cl B1 misses B2 by XBOOLE_0:def 7;
    hence thesis by A6,CONNSP_1:def 1;
  end;
  thus B1,B2 are_separated implies A1,A2 are_separated
  proof
    assume
A7: B1,B2 are_separated;
    then ((Cl A1) /\ [#]X0) misses A2 by A2,A4,CONNSP_1:def 1;
    then ((Cl A1) /\ [#]X0) /\ A2 = {} by XBOOLE_0:def 7;
    then
A8: (Cl A1 /\ A2) /\ [#]X0 = {} by XBOOLE_1:16;
    A1 misses ((Cl A2) /\ [#]X0) by A1,A3,A7,CONNSP_1:def 1;
    then A1 /\ ((Cl A2) /\ [#]X0) = {} by XBOOLE_0:def 7;
    then
A9: (A1 /\ Cl A2) /\ [#]X0 = {} by XBOOLE_1:16;
    A1 /\ Cl A2 c= A1 by XBOOLE_1:17;
    then A1 /\ Cl A2 = {} by A1,A9,XBOOLE_1:1,28;
    then
A10: A1 misses Cl A2 by XBOOLE_0:def 7;
    Cl A1 /\ A2 c= A2 by XBOOLE_1:17;
    then Cl A1 /\ A2 = {} by A2,A8,XBOOLE_1:1,28;
    then Cl A1 misses A2 by XBOOLE_0:def 7;
    hence thesis by A10,CONNSP_1:def 1;
  end;
end;

theorem Th26:
  B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2
  implies (A1,A2 are_separated implies B1,B2 are_separated)
proof
  assume
A1: B1 = (the carrier of X0) /\ A1;
  then reconsider C1 = B1 as Subset of X;
  assume
A2: B2 = (the carrier of X0) /\ A2;
  then
A3: B2 c= A2 by XBOOLE_1:17;
  reconsider C2 = B2 as Subset of X by A2;
  assume
A4: A1,A2 are_separated;
  B1 c= A1 by A1,XBOOLE_1:17;
  then C1,C2 are_separated by A3,A4,CONNSP_1:7;
  hence thesis by Th25;
end;

theorem Th27:
  B1 = A1 & B2 = A2 implies (A1,A2 are_weakly_separated iff B1,B2
  are_weakly_separated)
proof
  assume
A1: B1 = A1 & B2 = A2;
  thus A1,A2 are_weakly_separated implies B1,B2 are_weakly_separated
  proof
    assume A1,A2 are_weakly_separated;
    then A1 \ A2,A2 \ A1 are_separated by TSEP_1:def 5;
    then B1 \ B2,B2 \ B1 are_separated by A1,Th25;
    hence thesis by TSEP_1:def 5;
  end;
  thus B1,B2 are_weakly_separated implies A1,A2 are_weakly_separated
  proof
    assume B1,B2 are_weakly_separated;
    then B1 \ B2,B2 \ B1 are_separated by TSEP_1:def 5;
    then A1 \ A2,A2 \ A1 are_separated by A1,Th25;
    hence thesis by TSEP_1:def 5;
  end;
end;

theorem Th28:
  B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2
  implies (A1,A2 are_weakly_separated implies B1,B2 are_weakly_separated)
proof
  assume B1 = (the carrier of X0) /\ A1 & B2 = (the carrier of X0) /\ A2;
  then
A1: B1 \ B2 = (the carrier of X0) /\ (A1 \ A2) & B2 \ B1 = (the carrier of
  X0) /\ (A2 \ A1) by XBOOLE_1:50;
  assume A1 \ A2,A2 \ A1 are_separated;
  then B1 \ B2,B2 \ B1 are_separated by A1,Th26;
  hence thesis by TSEP_1:def 5;
end;

begin

:: 3. Certain Subspace-Decompositions of a Topological Space.

definition
  let X be non empty TopSpace, X1, X2 be SubSpace of X;
  pred X1,X2 constitute_a_decomposition means
  :Def2:
  for A1, A2 being Subset
  of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds A1,A2
  constitute_a_decomposition;
  symmetry;
end;

notation
  let X be non empty TopSpace, X1, X2 be SubSpace of X;
  antonym X1,X2 do_not_constitute_a_decomposition for X1,X2
  constitute_a_decomposition;
end;

reserve X0, X1, X2, Y1, Y2 for non empty SubSpace of X;

theorem Th29:
  X1,X2 constitute_a_decomposition iff X1 misses X2 & the
  TopStruct of X = X1 union X2
proof
  reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
  thus X1,X2 constitute_a_decomposition implies X1 misses X2 & the TopStruct
  of X = X1 union X2
  proof
    assume for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the
    carrier of X2 holds A1,A2 constitute_a_decomposition;
    then
A1: A1,A2 constitute_a_decomposition;
    then A1 misses A2 by Def1;
    hence X1 misses X2 by TSEP_1:def 3;
    A1 \/ A2 = the carrier of X by A1,Def1;
    then
A2: the carrier of X1 union X2 = the carrier of X by TSEP_1:def 2;
    X is SubSpace of X by TSEP_1:2;
    hence thesis by A2,TSEP_1:5;
  end;
  assume
A3: X1 misses X2;
  assume
A4: the TopStruct of X = X1 union X2;
  now
    let A1, A2 be Subset of X;
    assume A1 = the carrier of X1 & A2 = the carrier of X2;
    then A1 misses A2 & A1 \/ A2 = the carrier of X by A3,A4,TSEP_1:def 2,def 3
;
    hence A1,A2 constitute_a_decomposition by Def1;
  end;
  hence thesis by Def2;
end;

theorem Th30:
  X0,X0 do_not_constitute_a_decomposition
proof
  reconsider A0 = the carrier of X0 as Subset of X by TSEP_1:1;
  now
    take A1 = A0, A2 = A0;
    thus A1 = the carrier of X0 & A2 = the carrier of X0 & A1,A2
    do_not_constitute_a_decomposition by Th7;
  end;
  hence thesis by Def2;
end;

definition
  let X be non empty TopSpace, A1, A2 be non empty SubSpace of X;
  redefine pred A1,A2 constitute_a_decomposition;
  irreflexivity by Th30;
end;

theorem
  X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition
  implies the TopStruct of X1 = the TopStruct of X2
proof
  reconsider A0 = the carrier of X0, A1 = the carrier of X1, A2 = the carrier
  of X2 as Subset of X by TSEP_1:1;
  assume for A1, A0 being Subset of X st A1 = the carrier of X1 & A0 = the
  carrier of X0 holds A1,A0 constitute_a_decomposition;
  then
A1: A1,A0 constitute_a_decomposition;
  assume for A0, A2 being Subset of X st A0 = the carrier of X0 & A2 = the
  carrier of X2 holds A0,A2 constitute_a_decomposition;
  then A0,A2 constitute_a_decomposition;
  hence thesis by A1,Th8,TSEP_1:5;
end;

theorem Th32:
  for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1
constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds Y1 union Y2
  = the TopStruct of X iff X1 misses X2
proof
  let X1, X2, Y1, Y2 be non empty SubSpace of X;
  reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
  reconsider B1 = the carrier of Y1, B2 = the carrier of Y2 as Subset of X by
TSEP_1:1;
  assume that
A1: X1,Y1 constitute_a_decomposition and
A2: X2,Y2 constitute_a_decomposition;
A3: A2,B2 constitute_a_decomposition by A2,Def2;
  then
A4: A2 = B2` by Th3;
A5: A2 = B2` by A3,Th3;
A6: A1,B1 constitute_a_decomposition by A1,Def2;
  then
A7: A1 = B1` by Th3;
  thus Y1 union Y2 = the TopStruct of X implies X1 misses X2
  proof
    assume Y1 union Y2 = the TopStruct of X;
    then B1 \/ B2 = the carrier of X by TSEP_1:def 2;
    then (B1 \/ B2)` = {}X by XBOOLE_1:37;
    then A1 /\ A2 = {} by A7,A5,XBOOLE_1:53;
    then A1 misses A2 by XBOOLE_0:def 7;
    hence thesis by TSEP_1:def 3;
  end;
  assume X1 misses X2;
  then A1 misses A2 by TSEP_1:def 3;
  then
A8: A1 /\ A2 = {}X by XBOOLE_0:def 7;
  A1 = B1` by A6,Th3;
  then (B1 \/ B2)` = {}X by A4,A8,XBOOLE_1:53;
  then B1 \/ B2 = ({}X)`;
  then
A9: the carrier of Y1 union Y2 = the carrier of X by TSEP_1:def 2;
  X is SubSpace of X by TSEP_1:2;
  hence thesis by A9,TSEP_1:5;
end;

theorem Th33:
  X1,X2 constitute_a_decomposition implies (X1 is open iff X2 is closed)
proof
  reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
  assume
A1: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the
  carrier of X2 holds A1,A2 constitute_a_decomposition;
  thus X1 is open implies X2 is closed
  proof
    assume
A2: for A1 being Subset of X st A1 = the carrier of X1 holds A1 is open;
    now
      let A2 be Subset of X;
      assume A2 = the carrier of X2;
      then
A3:   A1,A2 constitute_a_decomposition by A1;
      A1 is open by A2;
      hence A2 is closed by A3,Th11;
    end;
    hence thesis by BORSUK_1:def 11;
  end;
  assume
A4: for A2 being Subset of X st A2 = the carrier of X2 holds A2 is closed;
  now
    let A1 be Subset of X;
    assume A1 = the carrier of X1;
    then
A5: A1,A2 constitute_a_decomposition by A1;
    A2 is closed by A4;
    hence A1 is open by A5,Th11;
  end;
  hence thesis by TSEP_1:def 1;
end;

theorem
  X1,X2 constitute_a_decomposition implies (X1 is closed iff X2 is open)
  by Th33;

theorem Th35:
  X1 meets Y1 & X1,X2 constitute_a_decomposition & Y1,Y2
  constitute_a_decomposition implies (X1 meet Y1),(X2 union Y2)
  constitute_a_decomposition
proof
  reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
  reconsider B1 = the carrier of Y1, B2 = the carrier of Y2 as Subset of X by
TSEP_1:1;
  assume
A1: X1 meets Y1;
  assume for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the
  carrier of X2 holds A1,A2 constitute_a_decomposition;
  then
A2: A1,A2 constitute_a_decomposition;
  assume for B1, B2 being Subset of X st B1 = the carrier of Y1 & B2 = the
  carrier of Y2 holds B1,B2 constitute_a_decomposition;
  then
A3: B1,B2 constitute_a_decomposition;
  now
    let C, D be Subset of X;
    assume C = the carrier of X1 meet Y1 & D = the carrier of X2 union Y2;
    then C = A1 /\ B1 & D = A2 \/ B2 by A1,TSEP_1:def 2,def 4;
    hence C,D constitute_a_decomposition by A2,A3,Th13;
  end;
  hence thesis by Def2;
end;

theorem
  X2 meets Y2 & X1,X2 constitute_a_decomposition & Y1,Y2
  constitute_a_decomposition implies (X1 union Y1),(X2 meet Y2)
  constitute_a_decomposition by Th35;

begin

:: 4. A Duality Between Pairs of Weakly Separated Subspaces.

reserve X for non empty TopSpace;

theorem Th37:
  for X1, X2, Y1, Y2 being SubSpace of X st X1,Y1
  constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds X1,X2
  are_weakly_separated implies Y1,Y2 are_weakly_separated
proof
  let X1, X2, Y1, Y2 be SubSpace of X;
  assume
A1: for A1, B1 being Subset of X st A1 = the carrier of X1 & B1 = the
  carrier of Y1 holds A1,B1 constitute_a_decomposition;
  assume
A2: for A2, B2 being Subset of X st A2 = the carrier of X2 & B2 = the
  carrier of Y2 holds A2,B2 constitute_a_decomposition;
  assume
A3: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the
  carrier of X2 holds A1,A2 are_weakly_separated;
  now
    reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X
    by TSEP_1:1;
    let B1, B2 be Subset of X;
    assume B1 = the carrier of Y1 & B2 = the carrier of Y2;
    then
A4: A1,B1 constitute_a_decomposition & A2,B2 constitute_a_decomposition by A1
,A2;
    A1,A2 are_weakly_separated by A3;
    hence B1,B2 are_weakly_separated by A4,Th15;
  end;
  hence thesis by TSEP_1:def 7;
end;

theorem
  for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1
  constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds X1,X2
  are_separated implies Y1,Y2 are_weakly_separated
proof
  let X1, X2, Y1, Y2 be non empty SubSpace of X;
  assume
A1: X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition;
  assume X1,X2 are_separated;
  then X1,X2 are_weakly_separated by TSEP_1:78;
  hence thesis by A1,Th37;
end;

theorem Th39:
  for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1
  constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds X1 misses
  X2 & Y1,Y2 are_weakly_separated implies X1,X2 are_separated
proof
  let X1, X2, Y1, Y2 be non empty SubSpace of X;
  assume
A1: X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition;
  assume
A2: X1 misses X2;
  assume Y1,Y2 are_weakly_separated;
  then X1,X2 are_weakly_separated by A1,Th37;
  hence thesis by A2,TSEP_1:78;
end;

theorem
  for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1
constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds Y1 union Y2
  = the TopStruct of X & Y1,Y2 are_weakly_separated implies X1,X2 are_separated
proof
  let X1, X2, Y1, Y2 be non empty SubSpace of X;
  assume
A1: X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition;
  assume Y1 union Y2 = the TopStruct of X;
  then
A2: X1 misses X2 by A1,Th32;
  assume Y1,Y2 are_weakly_separated;
  hence thesis by A1,A2,Th39;
end;

theorem
  for X1, X2 being non empty SubSpace of X st X1,X2
  constitute_a_decomposition holds (X1,X2 are_weakly_separated iff X1,X2
  are_separated)
proof
  let X1, X2 be non empty SubSpace of X;
  assume X1,X2 constitute_a_decomposition;
  then X1 misses X2 by Th29;
  hence thesis by TSEP_1:78;
end;

::An Enlargement Theorem for Subspaces.

theorem
  for X1, X2, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of
  X1 & Y2 is SubSpace of X2 & Y1 union Y2 = X1 union X2 holds Y1,Y2
  are_weakly_separated implies X1,X2 are_weakly_separated
proof
  let X1, X2, Y1, Y2 be non empty SubSpace of X;
  reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
  reconsider C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by
TSEP_1:1;
  assume Y1 is SubSpace of X1 & Y2 is SubSpace of X2;
  then
A1: C1 c= A1 & C2 c= A2 by TSEP_1:4;
  assume
A2: Y1 union Y2 = X1 union X2;
  assume Y1,Y2 are_weakly_separated;
  then
A3: C1,C2 are_weakly_separated by TSEP_1:def 7;
  now
    let A1, A2 be Subset of X;
    assume
A4: A1 = the carrier of X1 & A2 = the carrier of X2;
    then A1 \/ A2 = the carrier of X1 union X2 by TSEP_1:def 2;
    then A1 \/ A2 = C1 \/ C2 by A2,TSEP_1:def 2;
    hence A1,A2 are_weakly_separated by A1,A3,A4,Th22;
  end;
  hence thesis by TSEP_1:def 7;
end;

::An Extenuation Theorem for Subspaces.

theorem
  for X1, X2, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of
  X1 & Y2 is SubSpace of X2 & Y1 meets Y2 & Y1 meet Y2 = X1 meet X2 holds X1,X2
  are_weakly_separated implies Y1,Y2 are_weakly_separated
proof
  let X1, X2, Y1, Y2 be non empty SubSpace of X;
  reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
  reconsider C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by
TSEP_1:1;
  assume Y1 is SubSpace of X1 & Y2 is SubSpace of X2;
  then
A1: C1 c= A1 & C2 c= A2 by TSEP_1:4;
  assume
A2: Y1 meets Y2;
  assume
A3: Y1 meet Y2 = X1 meet X2;
  assume X1,X2 are_weakly_separated;
  then
A4: A1,A2 are_weakly_separated by TSEP_1:def 7;
  now
    let C1, C2 be Subset of X;
    assume
A5: C1 = the carrier of Y1 & C2 = the carrier of Y2;
    then C1 meets C2 by A2,TSEP_1:def 3;
    then C1 /\ C2 <> {} by XBOOLE_0:def 7;
    then A1 /\ A2 <> {} by A1,A5,XBOOLE_1:3,27;
    then A1 meets A2 by XBOOLE_0:def 7;
    then X1 meets X2 by TSEP_1:def 3;
    then A1 /\ A2 = the carrier of X1 meet X2 by TSEP_1:def 4;
    then A1 /\ A2 = C1 /\ C2 by A2,A3,A5,TSEP_1:def 4;
    hence C1,C2 are_weakly_separated by A1,A4,A5,Th24;
  end;
  hence thesis by TSEP_1:def 7;
end;

::Separated and Weakly Separated Subspaces in Subspaces.

reserve X0 for non empty SubSpace of X;

theorem Th44:
  for X1, X2 being SubSpace of X, Y1, Y2 being SubSpace of X0 st
  the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2
  holds X1,X2 are_separated iff Y1,Y2 are_separated
proof
  let X1, X2 be SubSpace of X, X01, X02 be SubSpace of X0;
  reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
  reconsider B1 = the carrier of X01, B2 = the carrier of X02 as Subset of X0
  by TSEP_1:1;
  assume
A1: the carrier of X1 = the carrier of X01 & the carrier of X2 = the
  carrier of X02;
  thus X1,X2 are_separated implies X01,X02 are_separated
  proof
    assume X1,X2 are_separated;
    then A1,A2 are_separated by TSEP_1:def 6;
    then for B1,B2 be Subset of X0 holds B1 = the carrier of X01 & B2 = the
    carrier of X02 implies B1,B2 are_separated by A1,Th25;
    hence thesis by TSEP_1:def 6;
  end;
  thus X01,X02 are_separated implies X1,X2 are_separated
  proof
    assume X01,X02 are_separated;
    then B1,B2 are_separated by TSEP_1:def 6;
    then for A1,A2 be Subset of X holds A1 = the carrier of X1 & A2 = the
    carrier of X2 implies A1,A2 are_separated by A1,Th25;
    hence thesis by TSEP_1:def 6;
  end;
end;

theorem
  for X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 holds X1,
  X2 are_separated implies Y1,Y2 are_separated
proof
  let X1, X2 be non empty SubSpace of X;
  assume
A1: X1 meets X0 & X2 meets X0;
  let Y1, Y2 be SubSpace of X0;
  assume
A2: Y1 = X1 meet X0 & Y2 = X2 meet X0;
  assume X1,X2 are_separated;
  then (X1 meet X0),(X2 meet X0) are_separated by A1,TSEP_1:70;
  hence thesis by A2,Th44;
end;

theorem
  for X1, X2 being SubSpace of X, Y1, Y2 being SubSpace of X0 st the
carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds
  X1,X2 are_weakly_separated iff Y1,Y2 are_weakly_separated
proof
  let X1, X2 be SubSpace of X, X01, X02 be SubSpace of X0;
  reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
  reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
  reconsider B1 = the carrier of X01 as Subset of X0 by TSEP_1:1;
  reconsider B2 = the carrier of X02 as Subset of X0 by TSEP_1:1;
  assume
A1: the carrier of X1 = the carrier of X01 & the carrier of X2 = the
  carrier of X02;
  thus X1,X2 are_weakly_separated implies X01,X02 are_weakly_separated
  proof
    assume X1,X2 are_weakly_separated;
    then A1,A2 are_weakly_separated by TSEP_1:def 7;
    then for B1,B2 be Subset of X0 holds B1 = the carrier of X01 & B2 = the
    carrier of X02 implies B1,B2 are_weakly_separated by A1,Th27;
    hence thesis by TSEP_1:def 7;
  end;
  thus X01,X02 are_weakly_separated implies X1,X2 are_weakly_separated
  proof
    assume X01,X02 are_weakly_separated;
    then B1,B2 are_weakly_separated by TSEP_1:def 7;
    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 A1,Th27;
    hence thesis by TSEP_1:def 7;
  end;
end;

theorem
  for X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0
for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 holds X1,
  X2 are_weakly_separated implies Y1,Y2 are_weakly_separated
proof
  let X1, X2 be non empty SubSpace of X;
  reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by
TSEP_1:1;
  assume
A1: X1 meets X0 & X2 meets X0;
  let Y1, Y2 be SubSpace of X0;
  assume
A2: Y1 = X1 meet X0 & Y2 = X2 meet X0;
  assume X1,X2 are_weakly_separated;
  then
A3: A1,A2 are_weakly_separated by TSEP_1:def 7;
  now
    let C1, C2 be Subset of X0;
    assume C1 = the carrier of Y1 & C2 = the carrier of Y2;
    then
    C1 = (the carrier of X0) /\ A1 & C2 = (the carrier of X0) /\ A2 by A1,A2,
TSEP_1:def 4;
    hence C1,C2 are_weakly_separated by A3,Th28;
  end;
  hence thesis by TSEP_1:def 7;
end;