Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992 Association of Mizar Users

### Separated and Weakly Separated Subspaces of Topological Spaces

by
Zbigniew Karno

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;

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);
```