:: Separated and Weakly Separated Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received January 8, 1992
:: Copyright (c) 1992-2021 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;
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;
registration
let X be TopSpace;
cluster strict open for SubSpace of X;
end;
registration
let X be non empty TopSpace;
cluster strict open non empty for 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 X1, X2 be 1-sorted;
pred X1 misses X2 means
:: TSEP_1:def 3
the carrier of X1 misses the carrier of X2;
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
X1 meets X2;
func X1 meet X2 -> strict non empty SubSpace of X means
:: TSEP_1:def 4
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.
theorem :: TSEP_1:26
(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:27
X1 meets X2 implies X1 meet X2 is SubSpace of X1 & X1 meet X2 is
SubSpace of X2;
theorem :: TSEP_1:28
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:29
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:30
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:31
X1 meets X2 implies X1 meet X2 is SubSpace of X1 union X2;
theorem :: TSEP_1:32
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:33
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.
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 :: TSEP_1:34
A1 is closed & A2 is closed implies (A1 misses A2 iff A1,A2 are_separated);
theorem :: TSEP_1:35
A1 \/ A2 is closed & A1,A2 are_separated implies A1 is closed & A2 is closed;
theorem :: TSEP_1:36
A1 misses A2 & A1 is open implies A1 misses Cl A2;
theorem :: TSEP_1:37
A1 is open & A2 is open implies (A1 misses A2 iff A1,A2 are_separated);
theorem :: TSEP_1:38
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:39
for C being Subset of X holds A1,A2 are_separated implies A1 /\
C,A2 /\ C are_separated;
theorem :: TSEP_1:40
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:41
for B being Subset of X holds A1,B are_separated & A2,B
are_separated iff A1 \/ A2,B are_separated;
theorem :: TSEP_1:42
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:43
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:44
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:45
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;
pred A1,A2 are_weakly_separated means
:: TSEP_1:def 5
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 :: TSEP_1:46
A1 misses A2 & A1,A2 are_weakly_separated iff A1,A2 are_separated;
theorem :: TSEP_1:47
A1 c= A2 implies A1,A2 are_weakly_separated;
theorem :: TSEP_1:48
for A1,A2 being Subset of X holds A1 is closed & A2 is closed
implies A1,A2 are_weakly_separated;
theorem :: TSEP_1:49
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:50
for C being Subset of X holds A1,A2 are_weakly_separated implies
A1 \/ C,A2 \/ C are_weakly_separated;
theorem :: TSEP_1:51
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:52
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:53
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:54
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:55
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:56
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:57
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:58
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:59
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:60
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:61
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:62
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 6
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 :: TSEP_1:63
X1,X2 are_separated implies X1 misses X2;
theorem :: TSEP_1:64
for X1, X2 being closed non empty SubSpace of X holds X1 misses X2 iff
X1,X2 are_separated;
theorem :: TSEP_1:65
X = X1 union X2 & X1,X2 are_separated implies X1 is closed SubSpace of X;
theorem :: TSEP_1:66
X1 union X2 is closed SubSpace of X & X1,X2 are_separated implies X1
is closed SubSpace of X;
theorem :: TSEP_1:67
for X1, X2 being open non empty SubSpace of X holds X1 misses X2 iff
X1,X2 are_separated;
theorem :: TSEP_1:68
X = X1 union X2 & X1,X2 are_separated implies X1 is open SubSpace of X;
theorem :: TSEP_1:69
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:70
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:71
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:72
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:73
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:74
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:75
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:76
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:77
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 7
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 :: TSEP_1:78
X1 misses X2 & X1,X2 are_weakly_separated iff X1,X2 are_separated;
theorem :: TSEP_1:79
X1 is SubSpace of X2 implies X1,X2 are_weakly_separated;
theorem :: TSEP_1:80
for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated;
theorem :: TSEP_1:81
for X1, X2 being open SubSpace of X holds X1,X2 are_weakly_separated;
::Extension Theorems for Weakly Separated Subspaces.
theorem :: TSEP_1:82
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:83
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:84
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:85
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:86
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:87
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:88
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:89
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:90
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:91
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:92
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);
theorem :: TSEP_1:93 :: WAYBEL34:30, AK, 20.02.2006
for T being TopStruct holds T|[#]T = the TopStruct of T;