The abstract of the Mizar article:

Separated and Weakly Separated Subspaces of Topological Spaces

by

Zbigniew Karno

Received January 8, 1992

MML identifier: TSEP_1

[ Mizar article, MML identifier index ]

environ

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


begin

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

theorem :: TSEP_1:1
 for X being TopStruct, X0 being SubSpace of X holds the carrier of X0
   is Subset of X;

theorem :: TSEP_1:2
 for X being TopStruct holds X is SubSpace of X;

theorem :: TSEP_1:3
   for X being strict TopStruct holds X|[#]X = X;

theorem :: TSEP_1:4
 for X1, X2 being SubSpace of X holds
  the carrier of X1 c= the carrier of X2 iff X1 is SubSpace of X2;

theorem :: TSEP_1:5
 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;

theorem :: TSEP_1:6
   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;

theorem :: TSEP_1:7
 for X1 being SubSpace of X for X2 being SubSpace of X1
 holds X2 is SubSpace of X;

theorem :: TSEP_1:8
 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;

theorem :: TSEP_1:9
 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;

theorem :: TSEP_1:10
 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;

::Properties of Closed Subspaces (for the definition see BORSUK_1:def 13).
theorem :: TSEP_1:11
 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;

theorem :: TSEP_1:12
   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;

theorem :: TSEP_1:13
   for X1 being closed SubSpace of X,
     X2 being closed SubSpace of X1 holds
  X2 is closed SubSpace of X;

theorem :: TSEP_1:14
   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;

theorem :: TSEP_1:15
 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;

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

definition let X be TopSpace;
 cluster strict open SubSpace of X;
end;

definition let X be non empty TopSpace;
 cluster strict open non empty SubSpace of X;
end;

::Properties of Open Subspaces.
theorem :: TSEP_1:16
 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;

theorem :: TSEP_1:17
   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;

theorem :: TSEP_1:18
   for X1 being open SubSpace of X,
     X2 being open SubSpace of X1 holds
  X2 is open SubSpace of X;

theorem :: TSEP_1:19
   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;

theorem :: TSEP_1:20
 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;


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
:: TSEP_1:def 2
  the carrier of it = (the carrier of X1) \/ (the carrier of X2);
 commutativity;
end;

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

::Properties of the Union of two Subspaces.
theorem :: TSEP_1:21
    (X1 union X2) union X3 = X1 union (X2 union X3);

theorem :: TSEP_1:22
 X1 is SubSpace of X1 union X2;

theorem :: TSEP_1:23
   for X1,X2 being non empty SubSpace of X holds
  X1 is SubSpace of X2 iff X1 union X2 = the TopStruct of X2;

theorem :: TSEP_1:24
   for X1, X2 being closed non empty SubSpace of X holds
  X1 union X2 is closed SubSpace of X;

theorem :: TSEP_1:25
   for X1, X2 being open non empty SubSpace of X holds
  X1 union X2 is open SubSpace of X;

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

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

  func X1 meet X2 -> strict non empty SubSpace of X means
:: TSEP_1:def 5
  the carrier of it = (the carrier of X1) /\ (the carrier of X2);
end;

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

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

theorem :: TSEP_1:29
 (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));

theorem :: TSEP_1:30
 X1 meets X2 implies
  X1 meet X2 is SubSpace of X1 & X1 meet X2 is SubSpace of X2;

theorem :: TSEP_1:31
   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);

theorem :: TSEP_1:32
   for X1, X2 being closed non empty SubSpace of X st X1 meets X2 holds
  X1 meet X2 is closed SubSpace of X;

theorem :: TSEP_1:33
   for X1, X2 being open non empty SubSpace of X st X1 meets X2 holds
  X1 meet X2 is open SubSpace of X;

::Connections between the Union and the Meet.
theorem :: TSEP_1:34
   X1 meets X2 implies
  X1 meet X2 is SubSpace of X1 union X2;

theorem :: TSEP_1:35
   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);

theorem :: TSEP_1:36
   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);


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

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

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

::Properties of Separated Subsets of Topological Spaces.
theorem :: TSEP_1:37
 for A1,A2 being Subset of X holds
  A1,A2 are_separated implies A1 misses A2;

theorem :: TSEP_1:38
 A1 is closed & A2 is closed implies (A1 misses A2 iff A1,A2 are_separated);

theorem :: TSEP_1:39
 A1 \/ A2 is closed & A1,A2 are_separated implies A1 is closed & A2 is closed;

theorem :: TSEP_1:40
 A1 misses A2 & A1 is open implies A1 misses Cl A2;

theorem :: TSEP_1:41
 A1 is open & A2 is open implies (A1 misses A2 iff A1,A2 are_separated);

theorem :: TSEP_1:42
 A1 \/ A2 is open & A1,A2 are_separated implies A1 is open & A2 is open;

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

theorem :: TSEP_1:43
 for C being Subset of X holds
  A1,A2 are_separated implies
  A1 /\ C,A2 /\ C are_separated;

theorem :: TSEP_1:44
 for B being Subset of X holds
   A1,B are_separated or A2,B are_separated implies A1 /\ A2,B are_separated;

theorem :: TSEP_1:45
 for B being Subset of X holds
  A1,B are_separated & A2,B are_separated iff A1 \/ A2,B are_separated;

theorem :: TSEP_1:46
 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;

::First Characterization of Separated Subsets of Topological Spaces.
theorem :: TSEP_1:47
 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;

theorem :: TSEP_1:48
 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;

::Second Characterization of Separated Subsets of Topological Spaces.
theorem :: TSEP_1:49
 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;

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

   pred A1,A2 are_weakly_separated means
:: TSEP_1:def 7
 A1 \ A2,A2 \ A1 are_separated;
 symmetry;
 antonym A1,A2 are_not_weakly_separated;
end;

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

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

theorem :: TSEP_1:51
 A1 misses A2 & A1,A2 are_weakly_separated iff A1,A2 are_separated;

theorem :: TSEP_1:52
 A1 c= A2 implies A1,A2 are_weakly_separated;

theorem :: TSEP_1:53
 for A1,A2 being Subset of X holds
  A1 is closed & A2 is closed implies A1,A2 are_weakly_separated;

theorem :: TSEP_1:54
 for A1,A2 being Subset of X holds
  A1 is open & A2 is open implies A1,A2 are_weakly_separated;

::Extension Theorems for Weakly Separated Subsets.
theorem :: TSEP_1:55
 for C being Subset of X holds
  A1,A2 are_weakly_separated implies
   A1 \/ C,A2 \/ C are_weakly_separated;

theorem :: TSEP_1:56
 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;

theorem :: TSEP_1:57
 for B being Subset of X holds
  A1,B are_weakly_separated & A2,B are_weakly_separated
    implies A1 /\ A2,B are_weakly_separated;

theorem :: TSEP_1:58
 for B being Subset of X holds
  A1,B are_weakly_separated & A2,B are_weakly_separated
    implies A1 \/ A2,B are_weakly_separated;

::First Characterization of Weakly Separated Subsets of Topological Spaces.
theorem :: TSEP_1:59
 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
;

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

theorem :: TSEP_1:60
 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);

theorem :: TSEP_1:61
 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);

theorem :: TSEP_1:62
 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);

::Second Characterization of Weakly Separated Subsets of Topological Spaces.
theorem :: TSEP_1:63
 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;

theorem :: TSEP_1:64
 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);

theorem :: TSEP_1:65
 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);

theorem :: TSEP_1:66
 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);

::A Characterization of Separated Subsets by means of Weakly Separated ones.
theorem :: TSEP_1:67
 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;


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
:: TSEP_1:def 8
 for A1, A2 being Subset of X st
  A1 = the carrier of X1 & A2 = the carrier of X2 holds
   A1,A2 are_separated;
 symmetry;
 antonym X1,X2 are_not_separated;
end;

reserve X1, X2 for non empty SubSpace of X;

::Properties of Separated Subspaces of Topological Spaces.
theorem :: TSEP_1:68
   X1,X2 are_separated implies X1 misses X2;

canceled;

theorem :: TSEP_1:70
   for X1, X2 being closed non empty SubSpace of X holds
  X1 misses X2 iff X1,X2 are_separated;

theorem :: TSEP_1:71
   X = X1 union X2 & X1,X2 are_separated implies
  X1 is closed SubSpace of X;

theorem :: TSEP_1:72
   X1 union X2 is closed SubSpace of X & X1,X2 are_separated implies
  X1 is closed SubSpace of X;

theorem :: TSEP_1:73
   for X1, X2 being open non empty SubSpace of X holds
  X1 misses X2 iff X1,X2 are_separated;

theorem :: TSEP_1:74
   X = X1 union X2 & X1,X2 are_separated implies
  X1 is open SubSpace of X;

theorem :: TSEP_1:75
   X1 union X2 is open SubSpace of X & X1,X2 are_separated implies
  X1 is open SubSpace of X;

::Restriction Theorems for Separated Subspaces.
theorem :: TSEP_1:76
   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;

theorem :: TSEP_1:77
 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;

theorem :: TSEP_1:78
   for Y being non empty SubSpace of X st X1 meets X2 holds
  X1,Y are_separated implies X1 meet X2,Y are_separated;

theorem :: TSEP_1:79
   for Y being non empty SubSpace of X holds
   X1,Y are_separated & X2,Y are_separated iff X1 union X2,Y are_separated;

theorem :: TSEP_1:80
   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;

::First Characterization of Separated Subspaces of Topological Spaces.
theorem :: TSEP_1:81
   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);

theorem :: TSEP_1:82
   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;

::Second Characterization of Separated Subspaces of Topological Spaces.
theorem :: TSEP_1:83
 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);

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

reserve X1, X2 for non empty SubSpace of X;

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

theorem :: TSEP_1:85
 X1 misses X2 & X1,X2 are_weakly_separated iff X1,X2 are_separated;

theorem :: TSEP_1:86
 X1 is SubSpace of X2 implies X1,X2 are_weakly_separated;

theorem :: TSEP_1:87
 for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated;

theorem :: TSEP_1:88
 for X1, X2 being open SubSpace of X holds X1,X2 are_weakly_separated;

::Extension Theorems for Weakly Separated Subspaces.
theorem :: TSEP_1:89
   for Y being non empty SubSpace of X holds
  X1,X2 are_weakly_separated implies
   X1 union Y,X2 union Y are_weakly_separated;

theorem :: TSEP_1:90
   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;

theorem :: TSEP_1:91
   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);

theorem :: TSEP_1:92
   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);

::First Characterization of Weakly Separated Subspaces of Topological Spaces.
theorem :: TSEP_1:93
   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)));

theorem :: TSEP_1:94
   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)));

theorem :: TSEP_1:95
   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);

::Second Characterization of Weakly Separated Subspaces of Topological Spaces.
theorem :: TSEP_1:96
   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)));

theorem :: TSEP_1:97
   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)));

theorem :: TSEP_1:98
   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);

::A Characterization of Separated Subspaces by means of Weakly Separated ones.
theorem :: TSEP_1:99
   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);