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