:: Separated and Weakly Separated Subspaces of Topological Spaces
:: by Zbigniew Karno
::
:: Received January 8, 1992
:: Copyright (c) 1992-2016 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;
definitions PRE_TOPC;
equalities SUBSET_1, STRUCT_0;
expansions PRE_TOPC;
theorems PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, BORSUK_1, SUBSET_1, XBOOLE_0,
XBOOLE_1;
begin
Lm1: for A being set for B,C,D being Subset of A st B \ C = {} holds B misses
(D \ C)
proof
let A be set;
let B,C,D be Subset of A;
assume B \ C = {};
then
A1: B c= C by XBOOLE_1:37;
C misses (D \ C) by XBOOLE_1:79;
hence thesis by A1,XBOOLE_1:63;
end;
Lm2: for A,B,C being set holds (A /\ B) \ C = (A \ C) /\ (B \ C)
proof
let A,B,C be set;
A1: (A \ C) misses C by XBOOLE_1:79;
thus (A /\ B) \ C = (A \ C) /\ B by XBOOLE_1:49
.= (A \ C) \ ((A \ C) \ B) by XBOOLE_1:48
.= (A \ C) \ (A \ (C \/ B)) by XBOOLE_1:41
.= ((A \ C) \ A) \/ ((A \ C) /\ (C \/ B)) by XBOOLE_1:52
.= {} \/ ((A \ C) /\ (C \/ B)) by XBOOLE_1:37
.= (A \ C) /\ ((B \ C) \/ C) by XBOOLE_1:39
.= (A \ C) /\ (B \ C) \/ (A \ C) /\ C by XBOOLE_1:23
.= (A \ C) /\ (B \ C) \/ {} by A1,XBOOLE_0:def 7
.= (A \ C) /\ (B \ C);
end;
::1. Some Properties of Subspaces of Topological Spaces.
reserve X for TopSpace;
theorem Th1:
for X being TopStruct, X0 being SubSpace of X holds the carrier
of X0 is Subset of X
proof
let X be TopStruct, X0 be SubSpace of X;
reconsider A = [#]X0 as Subset of [#]X by PRE_TOPC:def 4;
A c= [#]X;
hence thesis;
end;
theorem Th2:
for X being TopStruct holds X is SubSpace of X
proof
let X be TopStruct;
thus [#]X c= [#]X;
thus for P being Subset of X holds P in the topology of X iff ex Q being
Subset of X st Q in the topology of X & P = Q /\ [#]X
proof
let P be Subset of X;
thus P in the topology of X implies ex Q being Subset of X st Q in the
topology of X & P = Q /\ [#]X
proof
assume
A1: P in the topology of X;
take P;
thus thesis by A1,XBOOLE_1:28;
end;
thus thesis by XBOOLE_1:28;
end;
end;
theorem
for X being strict TopStruct holds X|[#]X = X
proof
let X be strict TopStruct;
reconsider X0 = X as SubSpace of X by Th2;
reconsider P = [#]X0 as Subset of X;
X|P = X0 by PRE_TOPC:def 5;
hence thesis;
end;
theorem Th4:
for X1, X2 being SubSpace of X holds the carrier of X1 c= the
carrier of X2 iff X1 is SubSpace of X2
proof
let X1, X2 be SubSpace of X;
set A1 = the carrier of X1, A2 = the carrier of X2;
A1: A1 = [#]X1;
A2: A2 = [#]X2;
thus the carrier of X1 c= the carrier of X2 implies X1 is SubSpace of X2
proof
assume
A3: A1 c= A2;
for P being Subset of X1 holds P in the topology of X1 iff ex Q being
Subset of X2 st Q in the topology of X2 & P = Q /\ A1
proof
let P be Subset of X1;
thus P in the topology of X1 implies ex Q being Subset of X2 st Q in the
topology of X2 & P = Q /\ A1
proof
assume P in the topology of X1;
then consider R being Subset of X such that
A4: R in the topology of X and
A5: P = R /\ A1 by A1,PRE_TOPC:def 4;
reconsider Q = R /\ A2 as Subset of X2 by XBOOLE_1:17;
take Q;
thus Q in the topology of X2 by A2,A4,PRE_TOPC:def 4;
Q /\ A1 = R /\ (A2 /\ A1) by XBOOLE_1:16
.= R /\ A1 by A3,XBOOLE_1:28;
hence thesis by A5;
end;
given Q being Subset of X2 such that
A6: Q in the topology of X2 and
A7: P = Q /\ A1;
consider R being Subset of X such that
A8: R in the topology of X and
A9: Q = R /\ [#]X2 by A6,PRE_TOPC:def 4;
P = R /\ (A2 /\ A1) by A7,A9,XBOOLE_1:16
.= R /\ A1 by A3,XBOOLE_1:28;
hence thesis by A1,A8,PRE_TOPC:def 4;
end;
hence thesis by A1,A2,A3,PRE_TOPC:def 4;
end;
thus thesis by A1,A2,PRE_TOPC:def 4;
end;
Lm3: for X being TopStruct, X0 being SubSpace of X holds the TopStruct of X0
is strict SubSpace of X
proof
let X be TopStruct, X0 be SubSpace of X;
set S = the TopStruct of X0;
S is SubSpace of X
proof
A1: [#] (X0) = the carrier of X0;
hence [#](S) c= [#](X) by PRE_TOPC:def 4;
let P be Subset of S;
thus P in the topology of S implies ex Q being Subset of X st Q in the
topology of X & P = Q /\ [#](S) by A1,PRE_TOPC:def 4;
given Q being Subset of X such that
A2: Q in the topology of X & P = Q /\ [#](S);
thus thesis by A1,A2,PRE_TOPC:def 4;
end;
hence thesis;
end;
theorem Th5:
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
proof
let X be TopStruct;
let X1, X2 be SubSpace of X;
reconsider S1 = the TopStruct of X1, S2 = the TopStruct of X2 as strict
SubSpace of X by Lm3;
set A1 = the carrier of X1, A2 = the carrier of X2;
assume
A1: A1 = A2;
A2: A1 = [#]S1;
A3: A2 = [#]S2;
reconsider A1 as Subset of X by BORSUK_1:1;
S1 = X|(A1) by A2,PRE_TOPC:def 5;
hence thesis by A1,A3,PRE_TOPC:def 5;
end;
theorem
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
proof
let X1,X2 be SubSpace of X;
set A1 = the carrier of X1, A2 = the carrier of X2;
assume X1 is SubSpace of X2 & X2 is SubSpace of X1;
then A1 c= A2 & A2 c= A1 by Th4;
then A1 = A2 by XBOOLE_0:def 10;
hence thesis by Th5;
end;
theorem Th7:
for X1 being SubSpace of X for X2 being SubSpace of X1 holds X2
is SubSpace of X
proof
let X1 be SubSpace of X;
let X2 be SubSpace of X1;
A1: [#]X2 c= [#]X1 by PRE_TOPC:def 4;
[#]X1 c= [#]X by PRE_TOPC:def 4;
hence [#](X2) c= [#](X) by A1,XBOOLE_1:1;
thus for P being Subset of X2 holds P in the topology of X2 iff ex Q being
Subset of X st Q in the topology of X & P = Q /\ [#]X2
proof
let P be Subset of X2;
reconsider P1 = P as Subset of X2;
thus P in the topology of X2 implies ex Q being Subset of X st Q in the
topology of X & P = Q /\ [#]X2
proof
assume P in the topology of X2;
then consider R being Subset of X1 such that
A2: R in the topology of X1 and
A3: P = R /\ [#]X2 by PRE_TOPC:def 4;
consider Q being Subset of X such that
A4: Q in the topology of X and
A5: R = Q /\ [#]X1 by A2,PRE_TOPC:def 4;
Q /\ [#]X2 = Q /\ ([#]X1 /\ [#]X2) by A1,XBOOLE_1:28
.= P by A3,A5,XBOOLE_1:16;
hence thesis by A4;
end;
given Q being Subset of X such that
A6: Q in the topology of X and
A7: P = Q /\ [#]X2;
reconsider R = Q /\ [#]X1 as Subset of X1;
reconsider Q1 = Q as Subset of X;
Q1 is open by A6;
then
A8: R is open by TOPS_2:24;
R /\ [#]X2 = Q /\ ([#]X1 /\ [#]X2) by XBOOLE_1:16
.= P by A1,A7,XBOOLE_1:28;
then P1 is open by A8,TOPS_2:24;
hence thesis;
end;
end;
theorem Th8:
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
proof
let X0 be SubSpace of X, C, A be Subset of X, B be Subset of X0 such that
A1: C is closed and
A2: C c= the carrier of X0 and
A3: A c= C and
A4: A = B;
thus B is closed implies A is closed
proof
assume B is closed;
then consider F being Subset of X such that
A5: F is closed and
A6: F /\ [#]X0 = B by PRE_TOPC:13;
A c= F by A4,A6,XBOOLE_1:17;
then
A7: A c= F /\ C by A3,XBOOLE_1:19;
F /\ C c= A by A2,A4,A6,XBOOLE_1:26;
hence thesis by A1,A5,A7,XBOOLE_0:def 10;
end;
thus thesis by A4,TOPS_2:26;
end;
theorem Th9:
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
proof
let X0 be SubSpace of X, C, A be Subset of X, B be Subset of X0 such that
A1: C is open and
A2: C c= the carrier of X0 and
A3: A c= C and
A4: A = B;
thus B is open implies A is open
proof
assume B is open;
then consider F being Subset of X such that
A5: F is open and
A6: F /\ [#]X0 = B by TOPS_2:24;
A c= F by A4,A6,XBOOLE_1:17;
then
A7: A c= F /\ C by A3,XBOOLE_1:19;
F /\ C c= A by A2,A4,A6,XBOOLE_1:26;
hence thesis by A1,A5,A7,XBOOLE_0:def 10;
end;
thus thesis by A4,TOPS_2:25;
end;
theorem Th10:
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
proof
let X be non empty TopStruct, A0 be non empty Subset of X;
take X0 = X|A0;
A0 = [#]X0 by PRE_TOPC:def 5;
hence thesis;
end;
::Properties of Closed Subspaces (for the definition see BORSUK_1:def 13).
theorem Th11:
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
proof
let X0 be SubSpace of X, A be Subset of X;
assume
A1: A = the carrier of X0;
hence X0 is closed SubSpace of X implies A is closed by BORSUK_1:def 11;
thus A is closed implies X0 is closed SubSpace of X
proof
assume A is closed;
then for B be Subset of X holds B = the carrier of X0 implies B is closed
by A1;
hence thesis by BORSUK_1:def 11;
end;
end;
theorem
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
proof
let X0 be closed SubSpace of X, A be Subset of X, B be Subset of X0 such
that
A1: A = B;
reconsider C = the carrier of X0 as Subset of X by Th1;
C is closed by Th11;
hence thesis by A1,Th8;
end;
theorem
for X1 being closed SubSpace of X, X2 being closed SubSpace of X1
holds X2 is closed SubSpace of X
proof
let X1 be closed SubSpace of X, X2 be closed SubSpace of X1;
now
reconsider C = [#]X1 as Subset of X by BORSUK_1:1;
let B be Subset of X;
assume
A1: B = the carrier of X2;
then reconsider BB = B as Subset of X1 by BORSUK_1:1;
BB is closed by A1,BORSUK_1:def 11;
then
A2: ex A being Subset of X st A is closed & A /\ [#]X1 = BB by PRE_TOPC:13;
C is closed by BORSUK_1:def 11;
hence B is closed by A2;
end;
hence thesis by Th7,BORSUK_1:def 11;
end;
theorem
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
proof
let X be non empty TopSpace, X1 be closed non empty SubSpace of X, X2 be non
empty SubSpace of X;
assume the carrier of X1 c= the carrier of X2;
then reconsider B = the carrier of X1 as Subset of X2;
now
let C be Subset of X2;
assume
A1: C = the carrier of X1;
then reconsider A = C as Subset of X by BORSUK_1:1;
A2: A /\ [#]X2 = C by XBOOLE_1:28;
A is closed by A1,Th11;
hence C is closed by A2,PRE_TOPC:13;
end;
then B is closed;
hence thesis by Th4,Th11;
end;
theorem Th15:
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
proof
let X be non empty TopSpace, A0 be non empty Subset of X such that
A1: A0 is closed;
consider X0 being strict non empty SubSpace of X such that
A2: A0 = the carrier of X0 by Th10;
reconsider Y0 = X0 as strict closed non empty SubSpace of X by A1,A2,Th11;
take Y0;
thus thesis by A2;
end;
definition
let X be TopStruct;
let IT be SubSpace of X;
attr IT is open means
:Def1:
for A being Subset of X st A = the carrier of IT holds A is open;
end;
Lm4: for T being TopStruct holds the TopStruct of T is SubSpace of T
proof
let T be TopStruct;
set S = the TopStruct of T;
thus [#]S c= [#]T;
let P be Subset of S;
hereby
reconsider Q = P as Subset of T;
assume
A1: P in the topology of S;
take Q;
thus Q in the topology of T by A1;
thus P = Q /\ [#]S by XBOOLE_1:28;
end;
given Q being Subset of T such that
A2: Q in the topology of T & P = Q /\ [#]S;
thus thesis by A2,XBOOLE_1:28;
end;
registration
let X be TopSpace;
cluster strict open for SubSpace of X;
existence
proof
reconsider Y = the TopStruct of X as strict SubSpace of X by Lm4;
take Y;
Y is open
proof
let A be Subset of X;
assume A = the carrier of Y;
then A = [#]X;
hence thesis;
end;
hence thesis;
end;
end;
registration
let X be non empty TopSpace;
cluster strict open non empty for SubSpace of X;
existence
proof
X|[#]X is open
proof
let A be Subset of X;
assume A = the carrier of X|[#]X;
then A = [#](X|[#]X) .= [#] X by PRE_TOPC:def 5;
hence thesis;
end;
hence thesis;
end;
end;
::Properties of Open Subspaces.
theorem Th16:
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
proof
let X0 be SubSpace of X, A be Subset of X;
assume
A1: A = the carrier of X0;
hence X0 is open SubSpace of X implies A is open by Def1;
thus A is open implies X0 is open SubSpace of X
proof
assume A is open;
then
for B be Subset of X holds B = the carrier of X0 implies B is open by A1;
hence thesis by Def1;
end;
end;
theorem
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
proof
let X0 be open SubSpace of X, A be Subset of X, B be Subset of X0 such that
A1: A = B;
reconsider C = the carrier of X0 as Subset of X by Th1;
C is open by Th16;
hence thesis by A1,Th9;
end;
theorem
for X1 being open SubSpace of X, X2 being open SubSpace of X1 holds X2
is open SubSpace of X
proof
let X1 be open SubSpace of X, X2 be open SubSpace of X1;
now
reconsider C = [#]X1 as Subset of X by BORSUK_1:1;
let B be Subset of X;
assume
A1: B = the carrier of X2;
then reconsider BB = B as Subset of X1 by BORSUK_1:1;
BB is open by A1,Def1;
then
A2: ex A being Subset of X st A is open & A /\ [#]X1 = BB by TOPS_2:24;
C is open by Def1;
hence B is open by A2;
end;
hence thesis by Def1,Th7;
end;
theorem
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
proof
let X be non empty TopSpace, X1 be open SubSpace of X, X2 be non empty
SubSpace of X;
assume the carrier of X1 c= the carrier of X2;
then reconsider B = the carrier of X1 as Subset of X2;
now
let C be Subset of X2;
assume
A1: C = the carrier of X1;
then reconsider A = C as Subset of X by BORSUK_1:1;
A2: A /\ [#]X2 = C by XBOOLE_1:28;
A is open by A1,Th16;
hence C is open by A2,TOPS_2:24;
end;
then B is open;
hence thesis by Th4,Th16;
end;
theorem Th20:
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
proof
let X be non empty TopSpace, A0 be non empty Subset of X such that
A1: A0 is open;
consider X0 being strict non empty SubSpace of X such that
A2: A0 = the carrier of X0 by Th10;
reconsider Y0 = X0 as strict open non empty SubSpace of X by A1,A2,Th16;
take Y0;
thus thesis by A2;
end;
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
:Def2:
the carrier of it = (the carrier of X1) \/ (the carrier of X2);
existence
proof
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X
by Th1;
set A = A1 \/ A2;
reconsider A as non empty Subset of X;
take X|A;
thus the carrier of (X|A) = [#](X|A)
.= (the carrier of X1) \/ (the carrier of X2) by PRE_TOPC:def 5;
end;
uniqueness by Th5;
commutativity;
end;
reserve X1, X2, X3 for non empty SubSpace of X;
::Properties of the Union of two Subspaces.
theorem
(X1 union X2) union X3 = X1 union (X2 union X3)
proof
the carrier of (X1 union X2) union X3 = (the carrier of X1 union X2) \/
(the carrier of X3) by Def2
.= ((the carrier of X1) \/ (the carrier of X2)) \/ (the carrier of X3)
by Def2
.= (the carrier of X1) \/ ((the carrier of X2) \/ (the carrier of X3))
by XBOOLE_1:4
.= (the carrier of X1) \/ (the carrier of X2 union X3) by Def2
.= the carrier of X1 union (X2 union X3) by Def2;
hence thesis by Th5;
end;
theorem Th22:
X1 is SubSpace of X1 union X2
proof
set A1 = the carrier of X1, A2 = the carrier of X2, A = the carrier of X1
union X2;
A = A1 \/ A2 by Def2;
then A1 c= A by XBOOLE_1:7;
hence thesis by Th4;
end;
theorem
for X1,X2 being non empty SubSpace of X holds X1 is SubSpace of X2 iff
X1 union X2 = the TopStruct of X2
proof
let X1,X2 be non empty SubSpace of X;
set A1 = the carrier of X1, A2 = the carrier of X2;
thus X1 is SubSpace of X2 iff X1 union X2 = the TopStruct of X2
proof
thus X1 is SubSpace of X2 implies X1 union X2 = the TopStruct of X2
proof
assume X1 is SubSpace of X2;
then
A1: A1 \/ A2 = the carrier of the TopStruct of X2 by BORSUK_1:1,XBOOLE_1:12;
the TopStruct of X2 is strict SubSpace of X by Lm3;
hence thesis by A1,Def2;
end;
assume X1 union X2 = the TopStruct of X2;
then A1 \/ A2 = A2 by Def2;
then A1 c= A2 by XBOOLE_1:7;
hence thesis by Th4;
end;
end;
theorem
for X1, X2 being closed non empty SubSpace of X holds X1 union X2 is
closed SubSpace of X
proof
let X1, X2 be closed non empty SubSpace of X;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A = the carrier of X1 union X2 as Subset of X by Th1;
A1 is closed & A2 is closed by Th11;
then A1 \/ A2 is closed;
then A is closed by Def2;
hence thesis by Th11;
end;
theorem
for X1, X2 being open non empty SubSpace of X holds X1 union X2 is
open SubSpace of X
proof
let X1, X2 be open non empty SubSpace of X;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A = the carrier of X1 union X2 as Subset of X by Th1;
A1 is open & A2 is open by Th16;
then A1 \/ A2 is open;
then A is open by Def2;
hence thesis by Th16;
end;
definition
let X1, X2 be 1-sorted;
pred X1 misses X2 means
the carrier of X1 misses the carrier of X2;
correctness;
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
A1: X1 meets X2;
func X1 meet X2 -> strict non empty SubSpace of X means
:Def4:
the carrier of it = (the carrier of X1) /\ (the carrier of X2);
existence
proof
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X
by Th1;
set A = A1 /\ A2;
A1 meets A2 by A1;
then reconsider A as non empty Subset of X by XBOOLE_0:def 7;
take X|A;
thus the carrier of (X|A) = [#](X|A)
.= (the carrier of X1) /\ (the carrier of X2) by PRE_TOPC:def 5;
end;
uniqueness by Th5;
end;
reserve X1, X2, X3 for non empty SubSpace of X;
::Properties of the Meet of two Subspaces.
theorem Th26:
(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))
proof
thus X1 meets X2 implies X1 meet X2 = X2 meet X1
proof
assume
A1: X1 meets X2;
then
the carrier of X1 meet X2 =(the carrier of X2) /\ (the carrier of X1)
by Def4
.= the carrier of X2 meet X1 by A1,Def4;
hence thesis by Th5;
end;
now
A2: now
assume that
A3: X1 meets X2 and
A4: (X1 meet X2) meets X3;
(the carrier of X1 meet X2) meets (the carrier of X3) by A4;
then (the carrier of X1 meet X2) /\ (the carrier of X3) <> {} by
XBOOLE_0:def 7;
then
((the carrier of X1) /\ (the carrier of X2)) /\ (the carrier of X3)
<> {} by A3,Def4;
then
A5: (the carrier of X1) /\ ((the carrier of X2) /\ (the carrier of X3))
<> {} by XBOOLE_1:16;
then (the carrier of X2) /\ (the carrier of X3) <> {};
then
A6: (the carrier of X2) meets (the carrier of X3) by XBOOLE_0:def 7;
then X2 meets X3;
then
(the carrier of X1) /\ (the carrier of X2 meet X3) <> {} by A5,Def4;
then (the carrier of X1) meets (the carrier of X2 meet X3) by
XBOOLE_0:def 7;
hence X1 meets X2 & (X1 meet X2) meets X3 & X2 meets X3 & X1 meets (X2
meet X3) by A3,A4,A6;
end;
assume
A7: X1 meets X2 & (X1 meet X2) meets X3 or X2 meets X3 & X1 meets (X2 meet X3);
A8: now
assume that
A9: X2 meets X3 and
A10: X1 meets (X2 meet X3);
(the carrier of X1) meets (the carrier of X2 meet X3) by A10;
then (the carrier of X1) /\ (the carrier of X2 meet X3) <> {} by
XBOOLE_0:def 7;
then
(the carrier of X1) /\ ((the carrier of X2) /\ (the carrier of X3))
<> {} by A9,Def4;
then
A11: ((the carrier of X1) /\ (the carrier of X2)) /\ (the carrier of X3)
<> {} by XBOOLE_1:16;
then (the carrier of X1) /\ (the carrier of X2) <> {};
then
A12: (the carrier of X1) meets (the carrier of X2) by XBOOLE_0:def 7;
then X1 meets X2;
then
(the carrier of X1 meet X2) /\ (the carrier of X3) <> {} by A11,Def4;
then (the carrier of X1 meet X2) meets (the carrier of X3) by
XBOOLE_0:def 7;
hence X1 meets X2 & (X1 meet X2) meets X3 & X2 meets X3 & X1 meets (X2
meet X3) by A9,A10,A12;
end;
then the carrier of (X1 meet X2) meet X3 = (the carrier of X1 meet X2) /\
(the carrier of X3) by A7,Def4
.= ((the carrier of X1) /\ (the carrier of X2)) /\ (the carrier of X3)
by A7,A8,Def4
.= (the carrier of X1) /\ ((the carrier of X2) /\ (the carrier of X3))
by XBOOLE_1:16
.= (the carrier of X1) /\ (the carrier of X2 meet X3) by A7,A2,Def4
.= the carrier of X1 meet (X2 meet X3) by A7,A2,Def4;
hence (X1 meet X2) meet X3 = X1 meet (X2 meet X3) by Th5;
end;
hence thesis;
end;
theorem Th27:
X1 meets X2 implies X1 meet X2 is SubSpace of X1 & X1 meet X2 is
SubSpace of X2
proof
assume X1 meets X2;
then the carrier of X1 meet X2 = (the carrier of X1) /\ (the carrier of X2)
by Def4;
then
the carrier of X1 meet X2 c= the carrier of X1 & the carrier of X1 meet
X2 c= the carrier of X2 by XBOOLE_1:17;
hence thesis by Th4;
end;
theorem
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)
proof
let X1,X2 be non empty SubSpace of X;
set A1 = the carrier of X1, A2 = the carrier of X2;
assume
A1: X1 meets X2;
thus X1 is SubSpace of X2 iff X1 meet X2 = the TopStruct of X1
proof
thus X1 is SubSpace of X2 implies X1 meet X2 = the TopStruct of X1
proof
assume X1 is SubSpace of X2;
then
A2: A1 /\ A2 = the carrier of the TopStruct of X1 by BORSUK_1:1,XBOOLE_1:28;
the TopStruct of X1 is strict SubSpace of X by Lm3;
hence thesis by A1,A2,Def4;
end;
assume X1 meet X2 = the TopStruct of X1;
then A1 /\ A2 = A1 by A1,Def4;
then A1 c= A2 by XBOOLE_1:17;
hence thesis by Th4;
end;
thus X2 is SubSpace of X1 iff X1 meet X2 = the TopStruct of X2
proof
thus X2 is SubSpace of X1 implies X1 meet X2 = the TopStruct of X2
proof
assume X2 is SubSpace of X1;
then
A3: A1 /\ A2 = the carrier of the TopStruct of X2 by BORSUK_1:1,XBOOLE_1:28;
the TopStruct of X2 is strict SubSpace of X by Lm3;
hence thesis by A1,A3,Def4;
end;
assume X1 meet X2 = the TopStruct of X2;
then A1 /\ A2 = A2 by A1,Def4;
then A2 c= A1 by XBOOLE_1:17;
hence thesis by Th4;
end;
end;
theorem
for X1, X2 being closed non empty SubSpace of X st X1 meets X2 holds
X1 meet X2 is closed SubSpace of X
proof
let X1, X2 be closed non empty SubSpace of X such that
A1: X1 meets X2;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A = the carrier of X1 meet X2 as Subset of X by Th1;
A1 is closed & A2 is closed by Th11;
then A1 /\ A2 is closed;
then A is closed by A1,Def4;
hence thesis by Th11;
end;
theorem
for X1, X2 being open non empty SubSpace of X st X1 meets X2 holds X1
meet X2 is open SubSpace of X
proof
let X1, X2 be open non empty SubSpace of X such that
A1: X1 meets X2;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider A = the carrier of X1 meet X2 as Subset of X by Th1;
A1 is open & A2 is open by Th16;
then A1 /\ A2 is open;
then A is open by A1,Def4;
hence thesis by Th16;
end;
::Connections between the Union and the Meet.
theorem
X1 meets X2 implies X1 meet X2 is SubSpace of X1 union X2
proof
assume X1 meets X2;
then
A1: X1 meet X2 is SubSpace of X1 by Th27;
X1 is SubSpace of X1 union X2 by Th22;
hence thesis by A1,Th7;
end;
theorem
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)
proof
let Y be non empty SubSpace of X;
assume that
A1: X1 meets Y and
A2: Y meets X2;
X1 is SubSpace of X1 union X2 by Th22;
then
A3: the carrier of X1 c= the carrier of X1 union X2 by Th4;
(the carrier of X1) meets (the carrier of Y) by A1;
then (the carrier of X1) /\ (the carrier of Y) <> {} by XBOOLE_0:def 7;
then (the carrier of X1 union X2) /\ (the carrier of Y) <> {} by A3,
XBOOLE_1:3,26;
then (the carrier of X1 union X2) meets (the carrier of Y) by XBOOLE_0:def 7;
then
A4: (X1 union X2) meets Y;
then
the carrier of (X1 union X2) meet Y = (the carrier of X1 union X2) /\ (
the carrier of Y) by Def4
.= ((the carrier of X1) \/ (the carrier of X2)) /\ (the carrier of Y) by
Def2
.= ((the carrier of X1) /\ (the carrier of Y)) \/ ((the carrier of X2)
/\ (the carrier of Y)) by XBOOLE_1:23
.= (the carrier of X1 meet Y) \/ ((the carrier of X2) /\ (the carrier of
Y)) by A1,Def4
.= (the carrier of X1 meet Y) \/ (the carrier of X2 meet Y) by A2,Def4
.= the carrier of (X1 meet Y) union (X2 meet Y) by Def2;
hence (X1 union X2) meet Y = (X1 meet Y) union (X2 meet Y) by Th5;
hence Y meet (X1 union X2) = (X1 meet Y) union (X2 meet Y) by A4,Th26
.= (Y meet X1) union (X2 meet Y) by A1,Th26
.= (Y meet X1) union (Y meet X2) by A2,Th26;
end;
theorem
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)
proof
let Y be non empty SubSpace of X;
assume
A1: X1 meets X2;
Y is SubSpace of X2 union Y by Th22;
then
A2: the carrier of Y c= the carrier of X2 union Y by Th4;
Y is SubSpace of X1 union Y by Th22;
then the carrier of Y c= the carrier of X1 union Y by Th4;
then (the carrier of X1 union Y) /\ (the carrier of X2 union Y) <> {} by A2,
XBOOLE_1:3,19;
then (the carrier of X1 union Y) meets (the carrier of X2 union Y) by
XBOOLE_0:def 7;
then
A3: (X1 union Y) meets (X2 union Y);
A4: the carrier of (X1 meet X2) union Y = (the carrier of X1 meet X2) \/ (
the carrier of Y) by Def2
.= ((the carrier of X1) /\ (the carrier of X2)) \/ (the carrier of Y) by A1
,Def4
.= ((the carrier of X1) \/ (the carrier of Y)) /\ ((the carrier of X2)
\/ (the carrier of Y)) by XBOOLE_1:24
.= (the carrier of X1 union Y) /\ ((the carrier of X2) \/ (the carrier
of Y)) by Def2
.= (the carrier of X1 union Y) /\ (the carrier of X2 union Y) by Def2
.= the carrier of (X1 union Y) meet (X2 union Y) by A3,Def4;
hence (X1 meet X2) union Y = (X1 union Y) meet (X2 union Y) by Th5;
thus thesis by A4,Th5;
end;
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 Th34:
A1 is closed & A2 is closed implies (A1 misses A2 iff A1,A2 are_separated)
proof
assume
A1: A1 is closed & A2 is closed;
thus A1 misses A2 implies A1,A2 are_separated
proof
assume
A2: A1 misses A2;
Cl A1 = A1 & Cl A2 = A2 by A1,PRE_TOPC:22;
hence thesis by A2,CONNSP_1:def 1;
end;
thus thesis by CONNSP_1:1;
end;
theorem Th35:
A1 \/ A2 is closed & A1,A2 are_separated implies A1 is closed & A2 is closed
proof
assume
A1: A1 \/ A2 is closed;
then Cl A1 c= A1 \/ A2 by TOPS_1:5,XBOOLE_1:7;
then
A2: Cl A1 \ A2 c= A1 by XBOOLE_1:43;
assume
A3: A1,A2 are_separated;
then Cl A1 misses A2 by CONNSP_1:def 1;
then
A4: Cl A1 c= A1 by A2,XBOOLE_1:83;
Cl A2 c= A1 \/ A2 by A1,TOPS_1:5,XBOOLE_1:7;
then
A5: Cl A2 \ A1 c= A2 by XBOOLE_1:43;
Cl A2 misses A1 by A3,CONNSP_1:def 1;
then
A6: Cl A2 c= A2 by A5,XBOOLE_1:83;
A1 c= Cl A1 & A2 c= Cl A2 by PRE_TOPC:18;
hence thesis by A6,A4,XBOOLE_0:def 10;
end;
theorem Th36:
A1 misses A2 & A1 is open implies A1 misses Cl A2
proof
assume
A1: A1 misses A2;
thus A1 is open implies A1 misses Cl A2
proof
assume
A2: A1 is open;
A2 c= A1` by A1,SUBSET_1:23;
then Cl A2 c= A1` by A2,TOPS_1:5;
then Cl A2 misses A1`` by SUBSET_1:24;
hence thesis;
end;
end;
theorem Th37:
A1 is open & A2 is open implies (A1 misses A2 iff A1,A2 are_separated)
proof
assume
A1: A1 is open & A2 is open;
thus A1 misses A2 implies A1,A2 are_separated
proof
assume A1 misses A2;
then A1 misses Cl A2 & Cl A1 misses A2 by A1,Th36;
hence thesis by CONNSP_1:def 1;
end;
thus thesis by CONNSP_1:1;
end;
theorem Th38:
A1 \/ A2 is open & A1,A2 are_separated implies A1 is open & A2 is open
proof
assume
A1: A1 \/ A2 is open;
A2: A1 c= Cl A1 by PRE_TOPC:18;
assume
A3: A1,A2 are_separated;
then A2 misses Cl A1 by CONNSP_1:def 1;
then
A4: A2 c= (Cl A1)` by SUBSET_1:23;
A1 misses Cl A2 by A3,CONNSP_1:def 1;
then
A5: A1 c= (Cl A2)` by SUBSET_1:23;
A6: A2 c= Cl A2 by PRE_TOPC:18;
A7: (A1 \/ A2) /\ (Cl A2)` = (A1 \/ A2) \ Cl A2 by SUBSET_1:13
.= (A1 \ Cl A2) \/ (A2 \ Cl A2) by XBOOLE_1:42
.= (A1 \ Cl A2) \/ {} by A6,XBOOLE_1:37
.= A1 /\ (Cl A2)` by SUBSET_1:13
.= A1 by A5,XBOOLE_1:28;
(A1 \/ A2) /\ (Cl A1)` = (A1 \/ A2) \ Cl A1 by SUBSET_1:13
.= (A1 \ Cl A1) \/ (A2 \ Cl A1) by XBOOLE_1:42
.= {} \/ (A2 \ Cl A1) by A2,XBOOLE_1:37
.= A2 /\ (Cl A1)` by SUBSET_1:13
.= A2 by A4,XBOOLE_1:28;
hence thesis by A1,A7;
end;
::A Restriction Theorem for Separated Subsets (see also CONNSP_1:8).
reserve A1,A2 for Subset of X;
theorem Th39:
for C being Subset of X holds A1,A2 are_separated implies A1 /\
C,A2 /\ C are_separated
proof
let C be Subset of X;
A1: A1 /\ C c= A1 & A2 /\ C c= A2 by XBOOLE_1:17;
assume A1,A2 are_separated;
hence thesis by A1,CONNSP_1:7;
end;
theorem Th40:
for B being Subset of X holds A1,B are_separated or A2,B
are_separated implies A1 /\ A2,B are_separated
proof
let B be Subset of X;
thus A1,B are_separated or A2,B are_separated implies A1 /\ A2,B
are_separated
proof
A1: now
A2: A1 /\ A2 c= A2 by XBOOLE_1:17;
assume A2,B are_separated;
hence thesis by A2,CONNSP_1:7;
end;
A3: now
A4: A1 /\ A2 c= A1 by XBOOLE_1:17;
assume A1,B are_separated;
hence thesis by A4,CONNSP_1:7;
end;
assume A1,B are_separated or A2,B are_separated;
hence thesis by A3,A1;
end;
end;
theorem Th41:
for B being Subset of X holds A1,B are_separated & A2,B
are_separated iff A1 \/ A2,B are_separated
proof
let B be Subset of X;
A1 \/ A2,B are_separated implies A1,B are_separated & A2,B are_separated
proof
A1: A1 c= A1 \/ A2 & A2 c= A1 \/ A2 by XBOOLE_1:7;
assume A1 \/ A2,B are_separated;
hence thesis by A1,CONNSP_1:7;
end;
hence
A1,B are_separated & A2,B are_separated iff A1 \/ A2,B are_separated by
CONNSP_1:8;
end;
theorem Th42:
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
proof
thus A1,A2 are_separated implies 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
proof
set C1 = Cl A1, C2 = Cl A2;
assume
A1: A1,A2 are_separated;
take C1,C2;
thus thesis by A1,CONNSP_1:def 1,PRE_TOPC:18;
end;
given C1, C2 being Subset of X such that
A2: A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed &
C2 is closed;
Cl A1 misses A2 & A1 misses Cl A2 by A2,TOPS_1:5,XBOOLE_1:63;
hence thesis by CONNSP_1:def 1;
end;
::First Characterization of Separated Subsets of Topological Spaces.
theorem Th43:
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
proof
thus A1,A2 are_separated implies 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
proof
assume A1,A2 are_separated;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 & A2 c= C2 and
A2: C1 misses A2 & C2 misses A1 and
A3: C1 is closed & C2 is closed by Th42;
take C1,C2;
C1 /\ C2 misses A1 & C1 /\ C2 misses A2 by A2,XBOOLE_1:17,63;
hence thesis by A1,A3,XBOOLE_1:70;
end;
given C1, C2 being Subset of X such that
A4: A1 c= C1 and
A5: A2 c= C2 and
A6: C1 /\ C2 misses A1 \/ A2 and
A7: C1 is closed & C2 is closed;
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
proof
take C1,C2;
A8: now
A1 /\ C2 c= C1 /\ C2 & A1 /\ C2 c= A1 by A4,XBOOLE_1:17,26;
then
A9: A1 /\ C2 c= (C1 /\ C2) /\ A1 by XBOOLE_1:19;
assume C2 meets A1;
then
A10: A1 /\ C2 <> {} by XBOOLE_0:def 7;
(C1 /\ C2) /\ A1 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:7,26;
then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A10,A9,XBOOLE_1:1,3;
hence contradiction by A6,XBOOLE_0:def 7;
end;
now
C1 /\ A2 c= C1 /\ C2 & C1 /\ A2 c= A2 by A5,XBOOLE_1:17,26;
then
A11: C1 /\ A2 c= (C1 /\ C2) /\ A2 by XBOOLE_1:19;
assume C1 meets A2;
then
A12: C1 /\ A2 <> {} by XBOOLE_0:def 7;
(C1 /\ C2) /\ A2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:7,26;
then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A12,A11,XBOOLE_1:1,3;
hence contradiction by A6,XBOOLE_0:def 7;
end;
hence thesis by A4,A5,A7,A8;
end;
hence thesis by Th42;
end;
theorem Th44:
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
proof
thus A1,A2 are_separated implies 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
proof
assume A1,A2 are_separated;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is closed &
C2 is closed by Th42;
take C2`,C1`;
thus thesis by A1,SUBSET_1:23,24;
end;
given C1, C2 being Subset of X such that
A2: A1 c= C1 & A2 c= C2 & C1 misses A2 & C2 misses A1 & C1 is open & C2
is open;
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
proof
take C2`,C1`;
thus thesis by A2,SUBSET_1:23,24;
end;
hence thesis by Th42;
end;
::Second Characterization of Separated Subsets of Topological Spaces.
theorem Th45:
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
proof
thus A1,A2 are_separated implies 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
proof
assume A1,A2 are_separated;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 & A2 c= C2 and
A2: C1 misses A2 & C2 misses A1 and
A3: C1 is open & C2 is open by Th44;
take C1,C2;
C1 /\ C2 misses A1 & C1 /\ C2 misses A2 by A2,XBOOLE_1:17,63;
hence thesis by A1,A3,XBOOLE_1:70;
end;
given C1, C2 being Subset of X such that
A4: A1 c= C1 and
A5: A2 c= C2 and
A6: C1 /\ C2 misses A1 \/ A2 and
A7: C1 is open & C2 is open;
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
proof
take C1,C2;
A8: now
A1 /\ C2 c= C1 /\ C2 & A1 /\ C2 c= A1 by A4,XBOOLE_1:17,26;
then
A9: A1 /\ C2 c= (C1 /\ C2) /\ A1 by XBOOLE_1:19;
assume C2 meets A1;
then
A10: A1 /\ C2 <> {} by XBOOLE_0:def 7;
(C1 /\ C2) /\ A1 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:7,26;
then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A10,A9,XBOOLE_1:1,3;
hence contradiction by A6,XBOOLE_0:def 7;
end;
now
C1 /\ A2 c= C1 /\ C2 & C1 /\ A2 c= A2 by A5,XBOOLE_1:17,26;
then
A11: C1 /\ A2 c= (C1 /\ C2) /\ A2 by XBOOLE_1:19;
assume C1 meets A2;
then
A12: C1 /\ A2 <> {} by XBOOLE_0:def 7;
(C1 /\ C2) /\ A2 c= (C1 /\ C2) /\ (A1 \/ A2) by XBOOLE_1:7,26;
then (C1 /\ C2) /\ (A1 \/ A2) <> {} by A12,A11,XBOOLE_1:1,3;
hence contradiction by A6,XBOOLE_0:def 7;
end;
hence thesis by A4,A5,A7,A8;
end;
hence thesis by Th44;
end;
definition
let X be TopStruct, A1, A2 be Subset of X;
pred A1,A2 are_weakly_separated means
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 Th46:
A1 misses A2 & A1,A2 are_weakly_separated iff A1,A2 are_separated
proof
thus A1 misses A2 & A1,A2 are_weakly_separated implies A1,A2 are_separated
proof
assume that
A1: A1 misses A2 and
A2: A1,A2 are_weakly_separated;
A1 \ A2 = A1 & A2 \ A1 = A2 by A1,XBOOLE_1:83;
hence thesis by A2;
end;
assume
A3: A1,A2 are_separated;
then A1 misses A2 by CONNSP_1:1;
then A1 \ A2 = A1 & A2 \ A1 = A2 by XBOOLE_1:83;
hence thesis by A3,CONNSP_1:1;
end;
theorem Th47:
A1 c= A2 implies A1,A2 are_weakly_separated
proof
A1: now
assume A1 c= A2;
then
A2: A1 \ A2 = {} by XBOOLE_1:37;
then Cl(A1 \ A2) = {} by PRE_TOPC:22;
then Cl(A1 \ A2) /\ (A2 \ A1) = {};
then
A3: Cl(A1 \ A2) misses (A2 \ A1) by XBOOLE_0:def 7;
(A1 \ A2) /\ Cl(A2 \ A1) = {} by A2;
then (A1 \ A2) misses Cl(A2 \ A1) by XBOOLE_0:def 7;
then A1 \ A2,A2 \ A1 are_separated by A3,CONNSP_1:def 1;
hence thesis;
end;
assume A1 c= A2;
hence thesis by A1;
end;
theorem Th48:
for A1,A2 being Subset of X holds A1 is closed & A2 is closed
implies A1,A2 are_weakly_separated
proof
let A1,A2 be Subset of X;
assume that
A1: A1 is closed and
A2: A2 is closed;
Cl(A2 \ A1) c= A2 by A2,TOPS_1:5,XBOOLE_1:36;
then Cl(A2 \ A1) \ A2 = {} by XBOOLE_1:37;
then
A3: (A1 \ A2) misses Cl(A2 \ A1) by Lm1;
Cl(A1 \ A2) c= A1 by A1,TOPS_1:5,XBOOLE_1:36;
then Cl(A1 \ A2) \ A1 = {} by XBOOLE_1:37;
then Cl(A1 \ A2) misses (A2 \ A1) by Lm1;
then A1 \ A2,A2 \ A1 are_separated by A3,CONNSP_1:def 1;
hence thesis;
end;
theorem Th49:
for A1,A2 being Subset of X holds A1 is open & A2 is open
implies A1,A2 are_weakly_separated
proof
let A1,A2 be Subset of X;
assume that
A1: A1 is open and
A2: A2 is open;
(A2 \ A1) misses A1 by XBOOLE_1:79;
then Cl(A2 \ A1) misses A1 by A1,Th36;
then
A3: (A1 \ A2) misses Cl(A2 \ A1) by XBOOLE_1:36,63;
A2 misses (A1 \ A2) by XBOOLE_1:79;
then A2 misses Cl(A1 \ A2) by A2,Th36;
then Cl(A1 \ A2) misses (A2 \ A1) by XBOOLE_1:36,63;
then A1 \ A2,A2 \ A1 are_separated by A3,CONNSP_1:def 1;
hence thesis;
end;
::Extension Theorems for Weakly Separated Subsets.
theorem Th50:
for C being Subset of X holds A1,A2 are_weakly_separated implies
A1 \/ C,A2 \/ C are_weakly_separated
proof
let C be Subset of X;
(A1 \/ C) \ (A2 \/ C) = (A1 \ (A2 \/ C)) \/ (C \ (A2 \/ C)) by XBOOLE_1:42
.= (A1 \ (A2 \/ C)) \/ {} by XBOOLE_1:46
.= (A1 \ A2) /\ (A1 \ C) by XBOOLE_1:53;
then
A1: (A1 \/ C) \ (A2 \/ C) c= A1 \ A2 by XBOOLE_1:17;
(A2 \/ C) \ (A1 \/ C) = (A2 \ (A1 \/ C)) \/ (C \ (A1 \/ C)) by XBOOLE_1:42
.= (A2 \ (A1 \/ C)) \/ {} by XBOOLE_1:46
.= (A2 \ A1) /\ (A2 \ C) by XBOOLE_1:53;
then
A2: (A2 \/ C) \ (A1 \/ C) c= A2 \ A1 by XBOOLE_1:17;
assume A1,A2 are_weakly_separated;
then A1 \ A2,A2 \ A1 are_separated;
then (A1 \/ C) \ (A2 \/ C),(A2 \/ C) \ (A1 \/ C) are_separated by A1,A2,
CONNSP_1:7;
hence thesis;
end;
theorem Th51:
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
proof
let B1, B2 be Subset of X such that
A1: B1 c= A2 and
A2: B2 c= A1;
A2 c= A2 \/ B2 by XBOOLE_1:7;
then B1 c= A2 \/ B2 by A1,XBOOLE_1:1;
then
A3: B1 \ (A2 \/ B2) = {} by XBOOLE_1:37;
A1 c= A1 \/ B1 by XBOOLE_1:7;
then B2 c= A1 \/ B1 by A2,XBOOLE_1:1;
then
A4: B2 \ (A1 \/ B1) = {} by XBOOLE_1:37;
(A2 \/ B2) \ (A1 \/ B1) = (A2 \ (A1 \/ B1)) \/ (B2 \ (A1 \/ B1)) by
XBOOLE_1:42;
then
A5: (A2 \/ B2) \ (A1 \/ B1) c= A2 \ A1 by A4,XBOOLE_1:7,34;
(A1 \/ B1) \ (A2 \/ B2) = (A1 \ (A2 \/ B2)) \/ (B1 \ (A2 \/ B2)) by
XBOOLE_1:42;
then
A6: (A1 \/ B1) \ (A2 \/ B2) c= A1 \ A2 by A3,XBOOLE_1:7,34;
assume A1,A2 are_weakly_separated;
then A1 \ A2,A2 \ A1 are_separated;
then (A1 \/ B1) \ (A2 \/ B2),(A2 \/ B2) \ (A1 \/ B1) are_separated by A6,A5,
CONNSP_1:7;
hence thesis;
end;
theorem Th52:
for B being Subset of X holds A1,B are_weakly_separated & A2,B
are_weakly_separated implies A1 /\ A2,B are_weakly_separated
proof
let B be Subset of X;
thus A1,B are_weakly_separated & A2,B are_weakly_separated implies A1 /\ A2,
B are_weakly_separated
proof
assume that
A1: A1,B are_weakly_separated and
A2: A2,B are_weakly_separated;
A2 \ B,B \ A2 are_separated by A2;
then
A3: (A1 \ B) /\ (A2 \ B),B \ A2 are_separated by Th40;
A1 \ B,B \ A1 are_separated by A1;
then (A1 \ B) /\ (A2 \ B),B \ A1 are_separated by Th40;
then (A1 \ B) /\ (A2 \ B),(B \ A1) \/ (B \ A2) are_separated by A3,Th41;
then (A1 /\ A2) \ B,(B \ A1) \/ (B \ A2) are_separated by Lm2;
then (A1 /\ A2) \ B,B \ (A1 /\ A2) are_separated by XBOOLE_1:54;
hence thesis;
end;
end;
theorem Th53:
for B being Subset of X holds A1,B are_weakly_separated & A2,B
are_weakly_separated implies A1 \/ A2,B are_weakly_separated
proof
let B be Subset of X;
thus A1,B are_weakly_separated & A2,B are_weakly_separated implies A1 \/ A2,
B are_weakly_separated
proof
assume that
A1: A1,B are_weakly_separated and
A2: A2,B are_weakly_separated;
A2 \ B,B \ A2 are_separated by A2;
then
A3: A2 \ B,(B \ A1) /\ (B \ A2) are_separated by Th40;
A1 \ B,B \ A1 are_separated by A1;
then A1 \ B,(B \ A1) /\ (B \ A2) are_separated by Th40;
then (A1 \ B) \/ (A2 \ B),(B \ A1) /\ (B \ A2) are_separated by A3,Th41;
then (A1 \/ A2) \ B,(B \ A1) /\ (B \ A2) are_separated by XBOOLE_1:42;
then (A1 \/ A2) \ B,B \ (A1 \/ A2) are_separated by XBOOLE_1:53;
hence thesis;
end;
end;
::First Characterization of Weakly Separated Subsets of Topological Spaces.
theorem Th54:
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
proof
set B1 = A1 \ A2, B2 = A2 \ A1;
A1: (A1 \/ A2)` misses (A1 \/ A2) by XBOOLE_1:79;
thus A1,A2 are_weakly_separated implies 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
proof
assume A1,A2 are_weakly_separated;
then B1,B2 are_separated;
then consider C1, C2 being Subset of X such that
A2: B1 c= C1 & B2 c= C2 and
A3: C1 misses B2 and
A4: C2 misses B1 and
A5: C1 is closed & C2 is closed by Th42;
C1 /\ B2 = {} by A3,XBOOLE_0:def 7;
then C1 /\ A2 \ C1 /\ A1 = {} by XBOOLE_1:50;
then
A6: C1 /\ A2 c= C1 /\ A1 by XBOOLE_1:37;
take C1,C2;
take C = (C1 \/ C2)`;
B1 \/ B2 c= C1 \/ C2 by A2,XBOOLE_1:13;
then C c= (B1 \/ B2)`by SUBSET_1:12;
then C c= (A1 \+\ A2)` by XBOOLE_0:def 6;
then C c= ((A1 \/ A2) \ A1 /\ A2)` by XBOOLE_1:101;
then C c= (A1 \/ A2)` \/ (A1 /\ A2) by SUBSET_1:14;
then C /\ (A1 \/ A2) c= ((A1 \/ A2)` \/ (A1 /\ A2)) /\ (A1 \/ A2) by
XBOOLE_1:26;
then C /\ (A1 \/ A2) c= (A1 \/ A2)` /\ (A1 \/ A2) \/ (A1 /\ A2) /\ (A1 \/
A2) by XBOOLE_1:23;
then
A7: C /\ (A1 \/ A2) c= {}X \/ (A1 /\ A2) /\ (A1 \/ A2) by A1,XBOOLE_0:def 7;
C2 /\ B1 = {} by A4,XBOOLE_0:def 7;
then C2 /\ A1 \ C2 /\ A2 = {} by XBOOLE_1:50;
then
A8: C2 /\ A1 c= C2 /\ A2 by XBOOLE_1:37;
C2 /\ (A1 \/ A2) = C2 /\ A1 \/ C2 /\ A2 by XBOOLE_1:23;
then
A9: C2 /\ (A1 \/ A2) = C2 /\ A2 by A8,XBOOLE_1:12;
C1 /\ (A1 \/ A2) = C1 /\ A1 \/ C1 /\ A2 by XBOOLE_1:23;
then
A10: C1 /\ (A1 \/ A2) = C1 /\ A1 by A6,XBOOLE_1:12;
[#]X = C \/ C` & (A1 /\ A2) /\ (A1 \/ A2) c= A1 /\ A2 by PRE_TOPC:2
,XBOOLE_1:17;
hence thesis by A5,A10,A9,A7,XBOOLE_1:1,17;
end;
given C1, C2, C being Subset of X such that
A11: C1 /\ (A1 \/ A2) c= A1 and
A12: C2 /\ (A1 \/ A2) c= A2 and
A13: C /\ (A1 \/ A2) c= A1 /\ A2 and
A14: the carrier of X = (C1 \/ C2) \/ C and
A15: C1 is closed & C2 is closed and
C is open;
ex C1 being Subset of X, C2 being Subset of X st B1 c= C1 & B2 c= C2 &
C1 /\ C2 misses B1 \/ B2 & C1 is closed & C2 is closed
proof
(C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2)) c= A1 /\ A2 by A11,A12,XBOOLE_1:27
;
then (C1 /\ ((A1 \/ A2) /\ C2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
then ((C1 /\ C2) /\ (A1 \/ A2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
then (C1 /\ C2) /\ ((A1 \/ A2) /\ (A1 \/ A2)) c= A1 /\ A2 by XBOOLE_1:16;
then ((C1 /\ C2) /\ (A1 \/ A2)) \ (A1 /\ A2) = {} by XBOOLE_1:37;
then (C1 /\ C2) /\ ((A1 \/ A2) \ (A1 /\ A2)) = {} by XBOOLE_1:49;
then
A16: (C1 /\ C2) /\ (B1 \/ B2) = {} by XBOOLE_1:55;
A1 /\ A2 c= A2 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A2 by A13,XBOOLE_1:1;
then C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A12,XBOOLE_1:8;
then
A17: (C2 \/ C) /\ (A1 \/ A2) c= A2 by XBOOLE_1:23;
A1 c= A1 \/ A2 by XBOOLE_1:7;
then B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by A17,XBOOLE_1:35;
then
A18: B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
A1 /\ A2 c= A1 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A1 by A13,XBOOLE_1:1;
then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 by A11,XBOOLE_1:8;
then
A19: (C \/ C1) /\ (A1 \/ A2) c= A1 by XBOOLE_1:23;
A2 c= A1 \/ A2 by XBOOLE_1:7;
then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) by A19,XBOOLE_1:35;
then
A20: B2 c= (A1 \/ A2) \ (C \/ C1) by XBOOLE_1:47;
take C1,C2;
A21: A1 \/ A2 c= [#]X;
then A1 \/ A2 c= (C2 \/ C) \/ C1 by A14,XBOOLE_1:4;
then
A22: (A1 \/ A2) \ (C2 \/ C) c= C1 by XBOOLE_1:43;
A1 \/ A2 c= (C \/ C1) \/ C2 by A14,A21,XBOOLE_1:4;
then (A1 \/ A2) \ (C \/ C1) c= C2 by XBOOLE_1:43;
hence thesis by A15,A20,A18,A22,A16,XBOOLE_0:def 7,XBOOLE_1:1;
end;
then B1,B2 are_separated by Th43;
hence thesis;
end;
reserve X for non empty TopSpace,
A1, A2 for Subset of X;
theorem Th55:
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)
proof
assume that
A1: A1,A2 are_weakly_separated and
A2: not A1 c= A2 and
A3: not A2 c= A1;
set B1 = A1 \ A2, B2 = A2 \ A1;
A4: B1 <> {} by A2,XBOOLE_1:37;
A5: B2 <> {} by A3,XBOOLE_1:37;
A6: A1 c= A1 \/ A2 by XBOOLE_1:7;
A7: A2 c= A1 \/ A2 by XBOOLE_1:7;
consider C1, C2, C being Subset of X such that
A8: C1 /\ (A1 \/ A2) c= A1 and
A9: C2 /\ (A1 \/ A2) c= A2 and
A10: C /\ (A1 \/ A2) c= A1 /\ A2 and
A11: the carrier of X = (C1 \/ C2) \/ C and
A12: C1 is closed & C2 is closed and
A13: C is open by A1,Th54;
A1 /\ A2 c= A1 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A1 by A10,XBOOLE_1:1;
then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 by A8,XBOOLE_1:8;
then (C \/ C1) /\ (A1 \/ A2) c= A1 by XBOOLE_1:23;
then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) by A7,XBOOLE_1:35;
then
A14: B2 c= (A1 \/ A2) \ (C \/ C1) by XBOOLE_1:47;
A1 /\ A2 c= A2 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A2 by A10,XBOOLE_1:1;
then C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:8;
then (C2 \/ C) /\ (A1 \/ A2) c= A2 by XBOOLE_1:23;
then B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by A6,XBOOLE_1:35;
then
A15: B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
A16: A1 \/ A2 c= [#]X;
then A1 \/ A2 c= (C \/ C1) \/ C2 by A11,XBOOLE_1:4;
then (A1 \/ A2) \ (C \/ C1) c= C2 by XBOOLE_1:43;
then reconsider D2 = C2 as non empty Subset of X by A14,A5,XBOOLE_1:1,3;
A1 \/ A2 c= (C2 \/ C) \/ C1 by A11,A16,XBOOLE_1:4;
then (A1 \/ A2) \ (C2 \/ C) c= C1 by XBOOLE_1:43;
then reconsider D1 = C1 as non empty Subset of X by A15,A4,XBOOLE_1:1,3;
take D1,D2;
now
assume
A17: not A1 \/ A2 c= C1 \/ C2;
thus ex C being non empty Subset of X st the carrier of X = (C1 \/ C2) \/
C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is open
proof
reconsider C0 = C as non empty Subset of X by A11,A17;
take C0;
thus thesis by A10,A11,A13;
end;
end;
hence thesis by A8,A9,A12;
end;
theorem Th56:
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)
proof
assume
A1: A1 \/ A2 = the carrier of X;
thus A1,A2 are_weakly_separated implies 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
proof
assume A1,A2 are_weakly_separated;
then consider C1, C2, C being Subset of X such that
A2: 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 by Th54;
take C1,C2,C;
thus thesis by A1,A2,XBOOLE_1:28;
end;
given C1, C2, C being Subset of X such that
A3: A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
C1 is closed & C2 is closed & C is open;
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
proof
take C1,C2,C;
thus thesis by A1,A3,XBOOLE_1:28;
end;
hence thesis by Th54;
end;
theorem Th57:
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)
proof
assume
A1: A1 \/ A2 = the carrier of X;
assume A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
then consider C1, C2 being non empty Subset of X such that
A2: C1 is closed & C2 is closed & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/
A2) c= A2 and
A3: 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 by
Th55;
take C1,C2;
now
assume not A1 \/ A2 = C1 \/ C2;
then consider C being non empty Subset of X such that
A4: C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1
\/ C2) \/ C by A1,A3,XBOOLE_0:def 10;
thus ex C being non empty Subset of X st A1 \/ A2 = (C1 \/ C2) \/ C & C c=
A1 /\ A2 & C is open
proof
take C;
thus thesis by A1,A4,XBOOLE_1:28;
end;
end;
hence thesis by A1,A2,XBOOLE_1:28;
end;
::Second Characterization of Weakly Separated Subsets of Topological Spaces.
theorem Th58:
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
proof
set B1 = A1 \ A2, B2 = A2 \ A1;
A1: (A1 \/ A2)` misses (A1 \/ A2) by XBOOLE_1:79;
thus A1,A2 are_weakly_separated implies 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
proof
assume A1,A2 are_weakly_separated;
then B1,B2 are_separated;
then consider C1, C2 being Subset of X such that
A2: B1 c= C1 & B2 c= C2 and
A3: C1 misses B2 and
A4: C2 misses B1 and
A5: C1 is open & C2 is open by Th44;
C1 /\ B2 = {} by A3,XBOOLE_0:def 7;
then C1 /\ A2 \ C1 /\ A1 = {} by XBOOLE_1:50;
then
A6: C1 /\ A2 c= C1 /\ A1 by XBOOLE_1:37;
take C1,C2;
take C = (C1 \/ C2)`;
B1 \/ B2 c= C1 \/ C2 by A2,XBOOLE_1:13;
then C c= (B1 \/ B2)`by SUBSET_1:12;
then C c= (A1 \+\ A2)` by XBOOLE_0:def 6;
then C c= ((A1 \/ A2) \ A1 /\ A2)` by XBOOLE_1:101;
then C c= (A1 \/ A2)` \/ (A1 /\ A2) by SUBSET_1:14;
then C /\ (A1 \/ A2) c= ((A1 \/ A2)` \/ (A1 /\ A2)) /\ (A1 \/ A2) by
XBOOLE_1:26;
then C /\ (A1 \/ A2) c= (A1 \/ A2)` /\ (A1 \/ A2) \/ (A1 /\ A2) /\ (A1 \/
A2) by XBOOLE_1:23;
then
A7: C /\ (A1 \/ A2) c= {}X \/ (A1 /\ A2) /\ (A1 \/ A2) by A1,XBOOLE_0:def 7;
C2 /\ B1 = {} by A4,XBOOLE_0:def 7;
then C2 /\ A1 \ C2 /\ A2 = {} by XBOOLE_1:50;
then
A8: C2 /\ A1 c= C2 /\ A2 by XBOOLE_1:37;
C2 /\ (A1 \/ A2) = C2 /\ A1 \/ C2 /\ A2 by XBOOLE_1:23;
then
A9: C2 /\ (A1 \/ A2) = C2 /\ A2 by A8,XBOOLE_1:12;
C1 /\ (A1 \/ A2) = C1 /\ A1 \/ C1 /\ A2 by XBOOLE_1:23;
then
A10: C1 /\ (A1 \/ A2) = C1 /\ A1 by A6,XBOOLE_1:12;
[#]X = C` \/ C & (A1 /\ A2) /\ (A1 \/ A2) c= A1 /\ A2 by PRE_TOPC:2
,XBOOLE_1:17;
hence thesis by A5,A10,A9,A7,XBOOLE_1:1,17;
end;
given C1, C2, C being Subset of X such that
A11: C1 /\ (A1 \/ A2) c= A1 and
A12: C2 /\ (A1 \/ A2) c= A2 and
A13: C /\ (A1 \/ A2) c= A1 /\ A2 and
A14: the carrier of X = (C1 \/ C2) \/ C and
A15: C1 is open & C2 is open and
C is closed;
ex C1, C2 being Subset of X st B1 c= C1 & B2 c= C2 & C1 /\ C2 misses B1
\/ B2 & C1 is open & C2 is open
proof
(C1 /\ (A1 \/ A2)) /\ (C2 /\ (A1 \/ A2)) c= A1 /\ A2 by A11,A12,XBOOLE_1:27
;
then (C1 /\ ((A1 \/ A2) /\ C2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
then ((C1 /\ C2) /\ (A1 \/ A2)) /\ (A1 \/ A2) c= A1 /\ A2 by XBOOLE_1:16;
then (C1 /\ C2) /\ ((A1 \/ A2) /\ (A1 \/ A2)) c= A1 /\ A2 by XBOOLE_1:16;
then ((C1 /\ C2) /\ (A1 \/ A2)) \ (A1 /\ A2) = {} by XBOOLE_1:37;
then (C1 /\ C2) /\ ((A1 \/ A2) \ (A1 /\ A2)) = {} by XBOOLE_1:49;
then
A16: (C1 /\ C2) /\ (B1 \/ B2) = {} by XBOOLE_1:55;
A1 /\ A2 c= A2 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A2 by A13,XBOOLE_1:1;
then C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A12,XBOOLE_1:8;
then
A17: (C2 \/ C) /\ (A1 \/ A2) c= A2 by XBOOLE_1:23;
A1 c= A1 \/ A2 by XBOOLE_1:7;
then B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by A17,XBOOLE_1:35;
then
A18: B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
A1 /\ A2 c= A1 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A1 by A13,XBOOLE_1:1;
then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 by A11,XBOOLE_1:8;
then
A19: (C \/ C1) /\ (A1 \/ A2) c= A1 by XBOOLE_1:23;
A2 c= A1 \/ A2 by XBOOLE_1:7;
then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) by A19,XBOOLE_1:35;
then
A20: B2 c= (A1 \/ A2) \ (C \/ C1) by XBOOLE_1:47;
take C1,C2;
A21: A1 \/ A2 c= [#]X;
then A1 \/ A2 c= (C2 \/ C) \/ C1 by A14,XBOOLE_1:4;
then
A22: (A1 \/ A2) \ (C2 \/ C) c= C1 by XBOOLE_1:43;
A1 \/ A2 c= (C \/ C1) \/ C2 by A14,A21,XBOOLE_1:4;
then (A1 \/ A2) \ (C \/ C1) c= C2 by XBOOLE_1:43;
hence thesis by A15,A20,A18,A22,A16,XBOOLE_0:def 7,XBOOLE_1:1;
end;
then B1,B2 are_separated by Th45;
hence thesis;
end;
theorem Th59:
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)
proof
assume that
A1: A1,A2 are_weakly_separated and
A2: not A1 c= A2 and
A3: not A2 c= A1;
set B1 = A1 \ A2, B2 = A2 \ A1;
A4: B1 <> {} by A2,XBOOLE_1:37;
A5: B2 <> {} by A3,XBOOLE_1:37;
A6: A1 c= A1 \/ A2 by XBOOLE_1:7;
A7: A2 c= A1 \/ A2 by XBOOLE_1:7;
consider C1, C2, C being Subset of X such that
A8: C1 /\ (A1 \/ A2) c= A1 and
A9: C2 /\ (A1 \/ A2) c= A2 and
A10: C /\ (A1 \/ A2) c= A1 /\ A2 and
A11: the carrier of X = (C1 \/ C2) \/ C and
A12: C1 is open & C2 is open and
A13: C is closed by A1,Th58;
A1 /\ A2 c= A1 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A1 by A10,XBOOLE_1:1;
then C /\ (A1 \/ A2) \/ C1 /\ (A1 \/ A2) c= A1 by A8,XBOOLE_1:8;
then (C \/ C1) /\ (A1 \/ A2) c= A1 by XBOOLE_1:23;
then B2 c= (A1 \/ A2) \ (C \/ C1) /\ (A1 \/ A2) by A7,XBOOLE_1:35;
then
A14: B2 c= (A1 \/ A2) \ (C \/ C1) by XBOOLE_1:47;
A1 /\ A2 c= A2 by XBOOLE_1:17;
then C /\ (A1 \/ A2) c= A2 by A10,XBOOLE_1:1;
then C2 /\ (A1 \/ A2) \/ C /\ (A1 \/ A2) c= A2 by A9,XBOOLE_1:8;
then (C2 \/ C) /\ (A1 \/ A2) c= A2 by XBOOLE_1:23;
then B1 c= (A1 \/ A2) \ (C2 \/ C) /\ (A1 \/ A2) by A6,XBOOLE_1:35;
then
A15: B1 c= (A1 \/ A2) \ (C2 \/ C) by XBOOLE_1:47;
A16: A1 \/ A2 c= [#]X;
then A1 \/ A2 c= (C \/ C1) \/ C2 by A11,XBOOLE_1:4;
then (A1 \/ A2) \ (C \/ C1) c= C2 by XBOOLE_1:43;
then reconsider D2 = C2 as non empty Subset of X by A14,A5,XBOOLE_1:1,3;
A1 \/ A2 c= (C2 \/ C) \/ C1 by A11,A16,XBOOLE_1:4;
then (A1 \/ A2) \ (C2 \/ C) c= C1 by XBOOLE_1:43;
then reconsider D1 = C1 as non empty Subset of X by A15,A4,XBOOLE_1:1,3;
take D1,D2;
now
assume
A17: not A1 \/ A2 c= C1 \/ C2;
thus ex C being non empty Subset of X st the carrier of X = (C1 \/ C2) \/
C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed
proof
reconsider C0 = C as non empty Subset of X by A11,A17;
take C0;
thus thesis by A10,A11,A13;
end;
end;
hence thesis by A8,A9,A12;
end;
theorem Th60:
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)
proof
assume
A1: A1 \/ A2 = the carrier of X;
thus A1,A2 are_weakly_separated implies 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
proof
assume A1,A2 are_weakly_separated;
then consider C1, C2, C being Subset of X such that
A2: 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 by Th58;
take C1,C2,C;
thus thesis by A1,A2,XBOOLE_1:28;
end;
given C1, C2, C being Subset of X such that
A3: A1 \/ A2 = (C1 \/ C2) \/ C & C1 c= A1 & C2 c= A2 & C c= A1 /\ A2 &
C1 is open & C2 is open & C is closed;
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
proof
take C1,C2,C;
thus thesis by A1,A3,XBOOLE_1:28;
end;
hence thesis by Th58;
end;
theorem Th61:
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)
proof
assume
A1: A1 \/ A2 = the carrier of X;
assume A1,A2 are_weakly_separated & not A1 c= A2 & not A2 c= A1;
then consider C1, C2 being non empty Subset of X such that
A2: C1 is open & C2 is open & C1 /\ (A1 \/ A2) c= A1 & C2 /\ (A1 \/ A2)
c= A2 and
A3: 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 by
Th59;
take C1,C2;
now
assume not A1 \/ A2 = C1 \/ C2;
then consider C being non empty Subset of X such that
A4: C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1
\/ C2 ) \/ C by A1,A3,XBOOLE_0:def 10;
thus ex C being non empty Subset of X st A1 \/ A2 = (C1 \/ C2) \/ C & C c=
A1 /\ A2 & C is closed
proof
take C;
thus thesis by A1,A4,XBOOLE_1:28;
end;
end;
hence thesis by A1,A2,XBOOLE_1:28;
end;
::A Characterization of Separated Subsets by means of Weakly Separated ones.
theorem Th62:
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
proof
thus A1,A2 are_separated implies ex B1, B2 being Subset of X st B1,B2
are_weakly_separated & A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2
proof
assume A1,A2 are_separated;
then consider B1, B2 being Subset of X such that
A1: A1 c= B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2 & B1 is open & B2
is open by Th45;
take B1,B2;
thus thesis by A1,Th49;
end;
given B1, B2 being Subset of X such that
A2: B1,B2 are_weakly_separated and
A3: A1 c= B1 and
A4: A2 c= B2 and
A5: B1 /\ B2 misses A1 \/ A2;
B1 /\ B2 misses A1 by A5,XBOOLE_1:7,63;
then
A6: (B1 /\ B2) /\ A1 = {} by XBOOLE_0:def 7;
B1 /\ B2 misses A2 by A5,XBOOLE_1:7,63;
then
A7: (B1 /\ B2) /\ A2 = {} by XBOOLE_0:def 7;
B1 /\ A2 c= A2 & B1 /\ A2 c= B1 /\ B2 by A4,XBOOLE_1:17,26;
then
A8: B1 /\ A2 = {} by A7,XBOOLE_1:3,19;
A2 \ B1 c= B2 \ B1 by A4,XBOOLE_1:33;
then
A9: A2 \ B1 /\ A2 c= B2 \ B1 by XBOOLE_1:47;
A1 /\ B2 c= A1 & A1 /\ B2 c= B1 /\ B2 by A3,XBOOLE_1:17,26;
then
A10: A1 /\ B2 = {} by A6,XBOOLE_1:3,19;
A1 \ B2 c= B1 \ B2 by A3,XBOOLE_1:33;
then
A11: A1 \ A1 /\ B2 c= B1 \ B2 by XBOOLE_1:47;
B1 \ B2,B2 \ B1 are_separated by A2;
hence thesis by A10,A8,A11,A9,CONNSP_1:7;
end;
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
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
X1,X2 are_separated implies X1 misses X2
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume X1,X2 are_separated;
then A1,A2 are_separated;
then A1 misses A2 by CONNSP_1:1;
hence thesis;
end;
theorem
for X1, X2 being closed non empty SubSpace of X holds X1 misses X2 iff
X1,X2 are_separated
proof
let X1, X2 be closed non empty SubSpace of X;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
A1: A1 is closed & A2 is closed by Th11;
thus X1 misses X2 implies X1,X2 are_separated
by A1,Th34;
assume X1,X2 are_separated;
then A1,A2 are_separated;
then A1 misses A2 by CONNSP_1:1;
hence thesis;
end;
theorem
X = X1 union X2 & X1,X2 are_separated implies X1 is closed SubSpace of X
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume X = X1 union X2;
then
A1: A1 \/ A2 = [#]X by Def2;
assume X1,X2 are_separated;
then A1,A2 are_separated;
then A1 is closed by A1,CONNSP_1:4;
hence thesis by Th11;
end;
theorem
X1 union X2 is closed SubSpace of X & X1,X2 are_separated implies X1
is closed SubSpace of X
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume
A1: X1 union X2 is closed SubSpace of X;
assume X1,X2 are_separated;
then
A2: A1,A2 are_separated;
A1 \/ A2 = the carrier of X1 union X2 by Def2;
then A1 \/ A2 is closed by A1,Th11;
then A1 is closed by A2,Th35;
hence thesis by Th11;
end;
theorem
for X1, X2 being open non empty SubSpace of X holds X1 misses X2 iff
X1,X2 are_separated
proof
let X1, X2 be open non empty SubSpace of X;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
A1: A1 is open & A2 is open by Th16;
thus X1 misses X2 implies X1,X2 are_separated
by A1,Th37;
assume X1,X2 are_separated;
then A1,A2 are_separated;
then A1 misses A2 by CONNSP_1:1;
hence thesis;
end;
theorem
X = X1 union X2 & X1,X2 are_separated implies X1 is open SubSpace of X
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume X = X1 union X2;
then
A1: A1 \/ A2 = [#]X by Def2;
assume X1,X2 are_separated;
then A1,A2 are_separated;
then A1 is open by A1,CONNSP_1:4;
hence thesis by Th16;
end;
theorem
X1 union X2 is open SubSpace of X & X1,X2 are_separated implies X1 is
open SubSpace of X
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume
A1: X1 union X2 is open SubSpace of X;
assume X1,X2 are_separated;
then
A2: A1,A2 are_separated;
A1 \/ A2 = the carrier of X1 union X2 by Def2;
then A1 \/ A2 is open by A1,Th16;
then A1 is open by A2,Th38;
hence thesis by Th16;
end;
::Restriction Theorems for Separated Subspaces.
theorem
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
proof
let Y, X1, X2 be non empty SubSpace of X such that
A1: X1 meets Y and
A2: X2 meets Y;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider C = the carrier of Y as Subset of X by Th1;
assume X1,X2 are_separated;
then
A3: A1,A2 are_separated;
now
let D1, D2 be Subset of X;
assume D1 = the carrier of X1 meet Y & D2 = the carrier of X2 meet Y;
then A1 /\ C = D1 & A2 /\ C = D2 by A1,A2,Def4;
hence D1,D2 are_separated by A3,Th39;
end;
hence X1 meet Y,X2 meet Y are_separated;
then X1 meet Y,Y meet X2 are_separated by A2,Th26;
hence Y meet X1,Y meet X2 are_separated by A1,Th26;
end;
theorem Th71:
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
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
let Y1, Y2 be SubSpace of X such that
A1: Y1 is SubSpace of X1 & Y2 is SubSpace of X2;
assume
A2: X1,X2 are_separated;
now
let B1, B2 be Subset of X;
assume B1 = the carrier of Y1 & B2 = the carrier of Y2;
then
A3: B1 c= A1 & B2 c= A2 by A1,Th4;
A1,A2 are_separated by A2;
hence B1,B2 are_separated by A3,CONNSP_1:7;
end;
hence thesis;
end;
theorem
for Y being non empty SubSpace of X st X1 meets X2 holds X1,Y
are_separated implies X1 meet X2,Y are_separated
proof
let Y be non empty SubSpace of X;
assume X1 meets X2;
then
A1: X1 meet X2 is SubSpace of X1 by Th27;
Y is SubSpace of Y by Th2;
hence thesis by A1,Th71;
end;
theorem
for Y being non empty SubSpace of X holds X1,Y are_separated & X2,Y
are_separated iff X1 union X2,Y are_separated
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
let Y be non empty SubSpace of X;
reconsider C = the carrier of Y as Subset of X by Th1;
A1: Y is SubSpace of Y by Th2;
thus X1,Y are_separated & X2,Y are_separated implies X1 union X2,Y
are_separated
proof
assume X1,Y are_separated & X2,Y are_separated;
then
A2: A1,C are_separated & A2,C are_separated;
now
let D, C be Subset of X;
assume that
A3: D = the carrier of X1 union X2 and
A4: C = the carrier of Y;
A1 \/ A2 = D by A3,Def2;
hence D,C are_separated by A2,A4,Th41;
end;
hence thesis;
end;
assume
A5: X1 union X2,Y are_separated;
X1 is SubSpace of X1 union X2 & X2 is SubSpace of X1 union X2 by Th22;
hence thesis by A5,A1,Th71;
end;
theorem
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
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
thus X1,X2 are_separated implies 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
proof
assume X1,X2 are_separated;
then A1,A2 are_separated;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 and
A2: A2 c= C2 and
A3: C1 misses A2 & C2 misses A1 and
A4: C1 is closed and
A5: C2 is closed by Th42;
C1 is non empty by A1,XBOOLE_1:3;
then consider Y1 being strict closed non empty SubSpace of X such that
A6: C1 = the carrier of Y1 by A4,Th15;
C2 is non empty by A2,XBOOLE_1:3;
then consider Y2 being strict closed non empty SubSpace of X such that
A7: C2 = the carrier of Y2 by A5,Th15;
take Y1,Y2;
thus thesis by A1,A2,A3,A6,A7,Th4;
end;
given Y1, Y2 being closed non empty SubSpace of X such that
A8: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1;
now
let A1, A2 be Subset of X such that
A9: A1 = the carrier of X1 & A2 = the carrier of X2;
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
proof
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
take C1,C2;
thus thesis by A8,A9,Th4,Th11;
end;
hence A1,A2 are_separated by Th42;
end;
hence thesis;
end;
::First Characterization of Separated Subspaces of Topological Spaces.
theorem
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)
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
thus X1,X2 are_separated implies 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)
proof
assume X1,X2 are_separated;
then A1,A2 are_separated;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 and
A2: A2 c= C2 and
A3: C1 /\ C2 misses A1 \/ A2 and
A4: C1 is closed and
A5: C2 is closed by Th43;
C1 is non empty by A1,XBOOLE_1:3;
then consider Y1 being strict closed non empty SubSpace of X such that
A6: C1 = the carrier of Y1 by A4,Th15;
C2 is non empty by A2,XBOOLE_1:3;
then consider Y2 being strict closed non empty SubSpace of X such that
A7: C2 = the carrier of Y2 by A5,Th15;
take Y1,Y2;
now
assume not Y1 misses Y2;
then
A8: the carrier of Y1 meet Y2 = C1 /\ C2 by A6,A7,Def4;
the carrier of X1 union X2 = A1 \/ A2 by Def2;
hence Y1 meet Y2 misses X1 union X2 by A3,A8;
end;
hence thesis by A1,A2,A6,A7,Th4;
end;
given Y1, Y2 being closed non empty SubSpace of X such that
A9: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A10: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
now
let A1, A2 be Subset of X such that
A11: A1 = the carrier of X1 & A2 = the carrier of X2;
ex C1 being Subset of X, C2 being Subset of X st A1 c= C1 & A2 c= C2
& C1 /\ C2 misses A1 \/ A2 & C1 is closed & C2 is closed
proof
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
take C1,C2;
now
per cases;
suppose
Y1 misses Y2;
then C1 misses C2;
then C1 /\ C2 = {} by XBOOLE_0:def 7;
hence C1 /\ C2 misses A1 \/ A2 by XBOOLE_1:65;
end;
suppose
A12: not Y1 misses Y2;
A13: the carrier of X1 union X2 = A1 \/ A2 by A11,Def2;
the carrier of Y1 meet Y2 = C1 /\ C2 by A12,Def4;
hence C1 /\ C2 misses A1 \/ A2 by A10,A12,A13;
end;
end;
hence thesis by A9,A11,Th4,Th11;
end;
hence A1,A2 are_separated by Th43;
end;
hence thesis;
end;
theorem
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
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
thus X1,X2 are_separated implies 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
proof
assume X1,X2 are_separated;
then A1,A2 are_separated;
then consider C1 being Subset of X, C2 being Subset of X such that
A1: A1 c= C1 and
A2: A2 c= C2 and
A3: C1 misses A2 & C2 misses A1 and
A4: C1 is open and
A5: C2 is open by Th44;
C1 is non empty by A1,XBOOLE_1:3;
then consider Y1 being strict open non empty SubSpace of X such that
A6: C1 = the carrier of Y1 by A4,Th20;
C2 is non empty by A2,XBOOLE_1:3;
then consider Y2 being strict open non empty SubSpace of X such that
A7: C2 = the carrier of Y2 by A5,Th20;
take Y1,Y2;
thus thesis by A1,A2,A3,A6,A7,Th4;
end;
given Y1, Y2 being open non empty SubSpace of X such that
A8: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 & Y1 misses X2 & Y2 misses X1;
now
let A1, A2 be Subset of X such that
A9: A1 = the carrier of X1 & A2 = the carrier of X2;
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
proof
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
take C1,C2;
thus thesis by A8,A9,Th4,Th16;
end;
hence A1,A2 are_separated by Th44;
end;
hence thesis;
end;
::Second Characterization of Separated Subspaces of Topological Spaces.
theorem Th77:
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)
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
thus X1,X2 are_separated implies 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)
proof
assume X1,X2 are_separated;
then A1,A2 are_separated;
then consider C1, C2 being Subset of X such that
A1: A1 c= C1 and
A2: A2 c= C2 and
A3: C1 /\ C2 misses A1 \/ A2 and
A4: C1 is open and
A5: C2 is open by Th45;
C1 is non empty by A1,XBOOLE_1:3;
then consider Y1 being strict open non empty SubSpace of X such that
A6: C1 = the carrier of Y1 by A4,Th20;
C2 is non empty by A2,XBOOLE_1:3;
then consider Y2 being strict open non empty SubSpace of X such that
A7: C2 = the carrier of Y2 by A5,Th20;
take Y1,Y2;
now
assume not Y1 misses Y2;
then
A8: the carrier of Y1 meet Y2 = C1 /\ C2 by A6,A7,Def4;
the carrier of X1 union X2 = A1 \/ A2 by Def2;
hence Y1 meet Y2 misses X1 union X2 by A3,A8;
end;
hence thesis by A1,A2,A6,A7,Th4;
end;
given Y1, Y2 being open non empty SubSpace of X such that
A9: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A10: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
now
let A1, A2 be Subset of X such that
A11: A1 = the carrier of X1 & A2 = the carrier of X2;
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
proof
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
take C1,C2;
now
per cases;
suppose
Y1 misses Y2;
then C1 misses C2;
then C1 /\ C2 = {} by XBOOLE_0:def 7;
hence C1 /\ C2 misses A1 \/ A2 by XBOOLE_1:65;
end;
suppose
A12: not Y1 misses Y2;
A13: the carrier of X1 union X2 = A1 \/ A2 by A11,Def2;
the carrier of Y1 meet Y2 = C1 /\ C2 by A12,Def4;
hence C1 /\ C2 misses A1 \/ A2 by A10,A12,A13;
end;
end;
hence thesis by A9,A11,Th4,Th16;
end;
hence A1,A2 are_separated by Th45;
end;
hence thesis;
end;
definition
let X be TopStruct, X1, X2 be SubSpace of X;
pred X1,X2 are_weakly_separated means
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 Th78:
X1 misses X2 & X1,X2 are_weakly_separated iff X1,X2 are_separated
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
thus X1 misses X2 & X1,X2 are_weakly_separated implies X1,X2 are_separated
by Th46;
assume X1,X2 are_separated;
then
A1: A1,A2 are_separated;
then A1 misses A2 by Th46;
hence X1 misses X2;
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,Th46;
hence thesis;
end;
theorem Th79:
X1 is SubSpace of X2 implies X1,X2 are_weakly_separated
by Th47,Th4;
theorem Th80:
for X1, X2 being closed SubSpace of X holds X1,X2 are_weakly_separated
proof
let X1, X2 be closed SubSpace of X;
let A1, A2 be Subset of X;
reconsider B1 = A1, B2 = A2 as Subset of X;
assume A1 = the carrier of X1 & A2 = the carrier of X2;
then B1 is closed & B2 is closed by Th11;
hence A1,A2 are_weakly_separated by Th48;
end;
theorem Th81:
for X1, X2 being open SubSpace of X holds X1,X2 are_weakly_separated
proof
let X1, X2 be open SubSpace of X;
let A1, A2 be Subset of X;
reconsider B1 = A1, B2 = A2 as Subset of X;
assume A1 = the carrier of X1 & A2 = the carrier of X2;
then B1 is open & B2 is open by Th16;
hence A1,A2 are_weakly_separated by Th49;
end;
::Extension Theorems for Weakly Separated Subspaces.
theorem
for Y being non empty SubSpace of X holds X1,X2 are_weakly_separated
implies X1 union Y,X2 union Y are_weakly_separated
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
let Y be non empty SubSpace of X;
reconsider C = the carrier of Y as Subset of X by Th1;
assume X1,X2 are_weakly_separated;
then
A1: A1,A2 are_weakly_separated;
now
let D1, D2 be Subset of X;
assume D1 = the carrier of X1 union Y & D2 = the carrier of X2 union Y;
then A1 \/ C = D1 & A2 \/ C = D2 by Def2;
hence D1,D2 are_weakly_separated by A1,Th50;
end;
hence thesis;
end;
theorem
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
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
let Y1, Y2 be non empty SubSpace of X such that
A1: Y1 is SubSpace of X2 & Y2 is SubSpace of X1;
reconsider B2 = the carrier of Y2 as Subset of X by Th1;
reconsider B1 = the carrier of Y1 as Subset of X by Th1;
assume X1,X2 are_weakly_separated;
then
A2: A1,A2 are_weakly_separated;
A3: B1 c= A2 & B2 c= A1 by A1,Th4;
A4: now
let D1, D2 be Subset of X;
assume D1 = the carrier of X1 union Y1 & D2 = the carrier of X2 union Y2;
then A1 \/ B1 = D1 & A2 \/ B2 = D2 by Def2;
hence D1,D2 are_weakly_separated by A3,A2,Th51;
end;
hence X1 union Y1,X2 union Y2 are_weakly_separated;
thus thesis by A4;
end;
theorem
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)
proof
let Y, X1, X2 be non empty SubSpace of X such that
A1: X1 meets X2;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
reconsider C = the carrier of Y as Subset of X by Th1;
thus X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1
meet X2,Y are_weakly_separated
proof
assume X1,Y are_weakly_separated & X2,Y are_weakly_separated;
then
A2: A1,C are_weakly_separated & A2,C are_weakly_separated;
now
let D, C be Subset of X;
assume that
A3: D = the carrier of X1 meet X2 and
A4: C = the carrier of Y;
A1 /\ A2 = D by A1,A3,Def4;
hence D,C are_weakly_separated by A2,A4,Th52;
end;
hence thesis;
end;
hence thesis;
end;
theorem
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)
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
let Y be non empty SubSpace of X;
reconsider C = the carrier of Y as Subset of X by Th1;
thus X1,Y are_weakly_separated & X2,Y are_weakly_separated implies X1
union X2,Y are_weakly_separated
proof
assume X1,Y are_weakly_separated & X2,Y are_weakly_separated;
then
A1: A1,C are_weakly_separated & A2,C are_weakly_separated;
now
let D, C be Subset of X;
assume that
A2: D = the carrier of X1 union X2 and
A3: C = the carrier of Y;
A1 \/ A2 = D by A2,Def2;
hence D,C are_weakly_separated by A1,A3,Th53;
end;
hence thesis;
end;
hence thesis;
end;
::First Characterization of Weakly Separated Subspaces of Topological Spaces.
theorem
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)))
proof
let X be non empty TopSpace, X1,X2 be non empty SubSpace of X;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume
A1: X1 meets X2;
A2: now
assume
A3: 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);
now
assume that
A4: not X1 is SubSpace of X2 and
A5: not X2 is SubSpace of X1;
consider Y1, Y2 being closed non empty SubSpace of X such that
A6: Y1 meet (X1 union X2) is SubSpace of X1 and
A7: Y2 meet (X1 union X2) is SubSpace of X2 and
A8: 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 by A3,A4,A5;
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
A9: the carrier of X1 union X2 = A1 \/ A2 by Def2;
A10: the carrier of Y1 union Y2 = C1 \/ C2 by Def2;
now
assume Y1 misses (X1 union X2);
then
A11: C1 misses (A1 \/ A2) by A9;
A12: now
per cases;
suppose
X1 union X2 is SubSpace of Y1 union Y2;
then A1 \/ A2 c= C1 \/ C2 by A9,A10,Th4;
then
A13: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ (C2 /\ (A1 \/ A2)) by A11,XBOOLE_0:def 7
.= C2 /\ (A1 \/ A2);
then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A9;
then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A9
,Def4;
hence A1 \/ A2 c= A2 by A7,A13,Th4;
end;
suppose
not X1 union X2 is SubSpace of Y1 union Y2;
then consider Y being open non empty SubSpace of X such that
A14: the TopStruct of X = (Y1 union Y2) union Y and
A15: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A8;
reconsider C = the carrier of Y as Subset of X by Th1;
the carrier of X = (C1 \/ C2) \/ C by A10,A14,Def2;
then
A16: A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A11,XBOOLE_0:def 7
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A17: now
assume C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A9;
then
A18: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A9,Def4;
the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
then
A19: C /\ (A1 \/ A2) c= A1 /\ A2 by A15,A18,Th4;
A20: A1 /\ A2 c= A2 by XBOOLE_1:17;
then
A21: C /\ (A1 \/ A2) c= A2 by A19,XBOOLE_1:1;
now
per cases;
suppose
C2 /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A2 by A16,A19,A20,XBOOLE_1:1;
end;
suppose
C2 /\ (A1 \/ A2) <> {};
then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A9;
then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2
) by A9,Def4;
then C2 /\ (A1 \/ A2) c= A2 by A7,Th4;
hence A1 \/ A2 c= A2 by A16,A21,XBOOLE_1:8;
end;
end;
hence A1 \/ A2 c= A2;
end;
now
assume C2 /\ (A1 \/ A2) <> {};
then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A9;
then
A22: the carrier of Y2 meet (X1 union X2) = C2 /\ ( A1 \/ A2) by A9
,Def4;
then
A23: C2 /\ (A1 \/ A2) c= A2 by A7,Th4;
now
per cases;
suppose
C /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A2 by A7,A16,A22,Th4;
end;
suppose
C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A9;
then
A24: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
by A9,Def4;
the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A15,A24,Th4;
then A1 \/ A2 c= A2 \/ A1 /\ A2 by A16,A23,XBOOLE_1:13;
hence A1 \/ A2 c= A2 by XBOOLE_1:12,17;
end;
end;
hence A1 \/ A2 c= A2;
end;
hence A1 \/ A2 c= A2 by A16,A17;
end;
end;
A1 c= A1 \/ A2 by XBOOLE_1:7;
then A1 c= A2 by A12,XBOOLE_1:1;
hence contradiction by A4,Th4;
end;
then
the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A9,Def4;
then
A25: C1 /\ (A1 \/ A2) c= A1 by A6,Th4;
now
assume not Y2 meets (X1 union X2);
then
A26: C2 misses (A1 \/ A2) by A9;
A27: now
per cases;
suppose
X1 union X2 is SubSpace of Y1 union Y2;
then A1 \/ A2 c= C1 \/ C2 by A9,A10,Th4;
then
A28: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ {} by A26,XBOOLE_0:def 7
.= C1 /\ (A1 \/ A2);
then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A9;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A9
,Def4;
hence A1 \/ A2 c= A1 by A6,A28,Th4;
end;
suppose
not X1 union X2 is SubSpace of Y1 union Y2;
then consider Y being open non empty SubSpace of X such that
A29: the TopStruct of X = (Y1 union Y2) union Y and
A30: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A8;
reconsider C = the carrier of Y as Subset of X by Th1;
the carrier of X = (C1 \/ C2) \/ C by A10,A29,Def2;
then
A31: A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A26,XBOOLE_0:def 7
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A32: now
assume C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A9;
then
A33: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A9,Def4;
the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
then
A34: C /\ (A1 \/ A2) c= A1 /\ A2 by A30,A33,Th4;
A35: A1 /\ A2 c= A1 by XBOOLE_1:17;
then
A36: C /\ (A1 \/ A2) c= A1 by A34,XBOOLE_1:1;
now
per cases;
suppose
C1 /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A1 by A31,A34,A35,XBOOLE_1:1;
end;
suppose
C1 /\ (A1 \/ A2) <> {};
then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A9;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2
) by A9,Def4;
then C1 /\ (A1 \/ A2) c= A1 by A6,Th4;
hence A1 \/ A2 c= A1 by A31,A36,XBOOLE_1:8;
end;
end;
hence A1 \/ A2 c= A1;
end;
now
assume C1 /\ (A1 \/ A2) <> {};
then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A9;
then
A37: the carrier of Y1 meet (X1 union X2) = C1 /\ ( A1 \/ A2)
by A9,Def4;
then
A38: C1 /\ (A1 \/ A2) c= A1 by A6,Th4;
now
per cases;
suppose
C /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A1 by A6,A31,A37,Th4;
end;
suppose
C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A9;
then
A39: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
by A9,Def4;
the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A30,A39,Th4;
then A1 \/ A2 c= A1 \/ A1 /\ A2 by A31,A38,XBOOLE_1:13;
hence A1 \/ A2 c= A1 by XBOOLE_1:12,17;
end;
end;
hence A1 \/ A2 c= A1;
end;
hence A1 \/ A2 c= A1 by A31,A32;
end;
end;
A2 c= A1 \/ A2 by XBOOLE_1:7;
then A2 c= A1 by A27,XBOOLE_1:1;
hence contradiction by A5,Th4;
end;
then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A9,Def4;
then
A40: C2 /\ (A1 \/ A2) c= A2 by A7,Th4;
A41: C1 is closed & C2 is closed by Th11;
now
per cases;
suppose
A42: A1 \/ A2 c= C1 \/ C2;
thus ex C being Subset of X st the carrier of X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 & C is open
proof
take C = (C1 \/ C2)`;
C misses (A1 \/ A2) by A42,SUBSET_1:24;
then C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
hence thesis by A41,PRE_TOPC:2,XBOOLE_1:2;
end;
end;
suppose
A43: not A1 \/ A2 c= C1 \/ C2;
thus ex C being Subset of X st the carrier of X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 & C is open
proof
consider Y being open non empty SubSpace of X such that
A44: the TopStruct of X = (Y1 union Y2) union Y and
A45: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A8,A9,A10,A43
,Th4;
reconsider C = the carrier of Y as Subset of X by Th1;
A46: the carrier of X = (the carrier of Y1 union Y2) \/ C by A44,Def2
.= (C1 \/ C2) \/ C by Def2;
now
assume not Y meets (X1 union X2);
then
A47: C misses (A1 \/ A2) by A9;
the carrier of X = (C1 \/ C2) \/ C by A10,A44,Def2;
then A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by
XBOOLE_1:23
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A47,XBOOLE_0:def 7
.= (C1 \/ C2) /\ (A1 \/ A2);
hence contradiction by A43,XBOOLE_1:17;
end;
then
A48: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A9,Def4;
A49: C is open by Th16;
the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A45,A48,Th4;
hence thesis by A49,A46;
end;
end;
end;
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 A41,A25,A40,Th54;
hence X1,X2 are_weakly_separated;
end;
hence X1,X2 are_weakly_separated by Th79;
end;
A50: X is SubSpace of X by Th2;
now
assume X1,X2 are_weakly_separated;
then
A51: A1,A2 are_weakly_separated;
now
assume that
A52: not X1 is SubSpace of X2 and
A53: not X2 is SubSpace of X1;
A54: not A2 c= A1 by A53,Th4;
A55: not A1 c= A2 by A52,Th4;
then consider C1, C2 being non empty Subset of X such that
A56: C1 is closed and
A57: C2 is closed and
A58: C1 /\ (A1 \/ A2) c= A1 and
A59: C2 /\ (A1 \/ A2) c= A2 and
A60: 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 by
A51,A54,Th55;
A61: now
assume C2 misses (A1 \/ A2);
then
A62: C2 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
now
per cases;
suppose
A63: A1 \/ A2 c= C1 \/ C2;
A64: A2 c= A1 \/ A2 by XBOOLE_1:7;
A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A63,XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ {} by A62,XBOOLE_1:23
.= C1 /\ (A1 \/ A2);
hence contradiction by A54,A58,A64,XBOOLE_1:1;
end;
suppose
not A1 \/ A2 c= C1 \/ C2;
then consider C being non empty Subset of X such that
C is open and
A65: C /\ (A1 \/ A2) c= A1 /\ A2 and
A66: the carrier of X = (C1 \/ C2) \/ C by A60;
A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A66,XBOOLE_1:28
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A62,XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
then A1 \/ A2 c= A1 \/ A1 /\ A2 by A58,A65,XBOOLE_1:13;
then
A67: A1 \/ A2 c= A1 by XBOOLE_1:12,17;
A2 c= A1 \/ A2 by XBOOLE_1:7;
hence contradiction by A54,A67,XBOOLE_1:1;
end;
end;
hence contradiction;
end;
A68: now
assume C1 misses (A1 \/ A2);
then
A69: C1 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
now
per cases;
suppose
A70: A1 \/ A2 c= C1 \/ C2;
A71: A1 c= A1 \/ A2 by XBOOLE_1:7;
A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A70,XBOOLE_1:28
.= {} \/ (C2 /\ (A1 \/ A2)) by A69,XBOOLE_1:23
.= C2 /\ (A1 \/ A2);
hence contradiction by A55,A59,A71,XBOOLE_1:1;
end;
suppose
not A1 \/ A2 c= C1 \/ C2;
then consider C being non empty Subset of X such that
C is open and
A72: C /\ (A1 \/ A2) c= A1 /\ A2 and
A73: the carrier of X = (C1 \/ C2) \/ C by A60;
A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A73,XBOOLE_1:28
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A69,XBOOLE_1:23
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
then A1 \/ A2 c= A2 \/ A1 /\ A2 by A59,A72,XBOOLE_1:13;
then
A74: A1 \/ A2 c= A2 by XBOOLE_1:12,17;
A1 c= A1 \/ A2 by XBOOLE_1:7;
hence contradiction by A55,A74,XBOOLE_1:1;
end;
end;
hence contradiction;
end;
thus 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)
proof
consider Y2 being strict closed non empty SubSpace of X such that
A75: C2 = the carrier of Y2 by A57,Th15;
A76: the carrier of X1 union X2 = A1 \/ A2 by Def2;
then Y2 meets (X1 union X2) by A61,A75;
then
A77: the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A75,A76,Def4
;
consider Y1 being strict closed non empty SubSpace of X such that
A78: C1 = the carrier of Y1 by A56,Th15;
A79: the carrier of Y1 union Y2 = C1 \/ C2 by A78,A75,Def2;
A80: now
assume
A81: not X1 union X2 is SubSpace of Y1 union Y2;
then consider C being non empty Subset of X such that
A82: C is open and
A83: C /\ (A1 \/ A2) c= A1 /\ A2 and
A84: the carrier of X = (C1 \/ C2) \/ C by A60,A76,A79,Th4;
A85: not A1 \/ A2 c= C1 \/ C2 by A76,A79,A81,Th4;
thus 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
proof
consider Y being strict open non empty SubSpace of X such that
A86: C = the carrier of Y by A82,Th20;
now
assume C misses (A1 \/ A2);
then
A87: C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A84,XBOOLE_1:28
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A87,XBOOLE_1:23
.= (C1 \/ C2) /\ (A1 \/ A2);
hence contradiction by A85,XBOOLE_1:17;
end;
then Y meets (X1 union X2) by A76,A86;
then
A88: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A76,A86
,Def4;
take Y;
A89: the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
the carrier of X = (the carrier of Y1 union Y2) \/ C by A78,A75,A84
,Def2
.= the carrier of (Y1 union Y2) union Y by A86,Def2;
hence thesis by A50,A83,A88,A89,Th4,Th5;
end;
end;
take Y1,Y2;
Y1 meets (X1 union X2) by A68,A78,A76;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A78,A76
,Def4;
hence thesis by A58,A59,A77,A80,Th4;
end;
end;
hence 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);
end;
hence thesis by A2;
end;
theorem
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)))
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume
A1: X = X1 union X2;
then
A2: A1 \/ A2 = the carrier of X by Def2;
assume
A3: X1 meets X2;
A4: now
assume
A5: X1 is SubSpace of X2 or X2 is SubSpace of X1 or (not X1 is
SubSpace of X2 & not X2 is SubSpace of X1 implies 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));
now
assume ( not X1 is SubSpace of X2)& not X2 is SubSpace of X1;
then consider Y1, Y2 being closed non empty SubSpace of X such that
A6: Y1 is SubSpace of X1 & Y2 is SubSpace of X2 and
A7: 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 by A5;
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
A8: now
per cases;
suppose
A9: A1 \/ A2 = C1 \/ C2;
thus ex C being Subset of X st A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1
/\ A2 & C is open
proof
take {}X;
thus thesis by A9,XBOOLE_1:2;
end;
end;
suppose
A10: A1 \/ A2 <> C1 \/ C2;
thus ex C being Subset of X st A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1
/\ A2 & C is open
proof
consider Y being open non empty SubSpace of X such that
A11: X = (Y1 union Y2) union Y and
A12: Y is SubSpace of X1 meet X2 by A2,A7,A10,Def2;
reconsider C = the carrier of Y as Subset of X by Th1;
A1 /\ A2 = the carrier of X1 meet X2 by A3,Def4;
then
A13: C c= A1 /\ A2 by A12,Th4;
A14: C is open by Th16;
A1 \/ A2 = (the carrier of Y1 union Y2) \/ C by A2,A11,Def2
.= (C1 \/ C2) \/ C by Def2;
hence thesis by A14,A13;
end;
end;
end;
A15: C1 is closed & C2 is closed by Th11;
C1 c= A1 & C2 c= A2 by A6,Th4;
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 A2,A15,A8,Th56;
hence X1,X2 are_weakly_separated;
end;
hence X1,X2 are_weakly_separated by Th79;
end;
now
assume X1,X2 are_weakly_separated;
then
A16: A1,A2 are_weakly_separated;
now
assume ( not X1 is SubSpace of X2)& not X2 is SubSpace of X1;
then ( not A1 c= A2)& not A2 c= A1 by Th4;
then consider C1, C2 being non empty Subset of X such that
A17: C1 is closed and
A18: C2 is closed and
A19: C1 c= A1 & C2 c= A2 and
A20: 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 by A2,A16,Th57;
thus 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)
proof
consider Y2 being strict closed non empty SubSpace of X such that
A21: C2 = the carrier of Y2 by A18,Th15;
consider Y1 being strict closed non empty SubSpace of X such that
A22: C1 = the carrier of Y1 by A17,Th15;
take Y1,Y2;
now
assume X <> Y1 union Y2;
then consider C being non empty Subset of X such that
A23: A1 \/ A2 = (C1 \/ C2) \/ C and
A24: C c= A1 /\ A2 and
A25: C is open by A1,A2,A20,A22,A21,Def2;
thus ex Y being open non empty SubSpace of X st X = (Y1 union Y2)
union Y & Y is SubSpace of X1 meet X2
proof
A26: C c= the carrier of X1 meet X2 by A3,A24,Def4;
consider Y being strict open non empty SubSpace of X such that
A27: C = the carrier of Y by A25,Th20;
take Y;
the carrier of X = (the carrier of Y1 union Y2) \/ C by A2,A22,A21
,A23,Def2
.= the carrier of (Y1 union Y2) union Y by A27,Def2;
hence thesis by A1,A27,A26,Th4,Th5;
end;
end;
hence thesis by A19,A22,A21,Th4;
end;
end;
hence 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);
end;
hence thesis by A4;
end;
theorem
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)
proof
assume
A1: X = X1 union X2;
assume
A2: X1 misses X2;
thus X1,X2 are_weakly_separated implies X1 is closed SubSpace of X & X2 is
closed SubSpace of X
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume X1,X2 are_weakly_separated;
then X1,X2 are_separated by A2,Th78;
then
A3: A1,A2 are_separated;
A1 \/ A2 = [#]X by A1,Def2;
then A1 is closed & A2 is closed by A3,CONNSP_1:4;
hence thesis by Th11;
end;
thus thesis by Th80;
end;
::Second Characterization of Weakly Separated Subspaces of Topological Spaces.
theorem
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)))
proof
let X be non empty TopSpace, X1,X2 be non empty SubSpace of X;
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume
A1: X1 meets X2;
A2: [#]X = the carrier of X;
A3: now
assume
A4: 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);
now
assume that
A5: not X1 is SubSpace of X2 and
A6: not X2 is SubSpace of X1;
consider Y1, Y2 being open non empty SubSpace of X such that
A7: Y1 meet (X1 union X2) is SubSpace of X1 and
A8: Y2 meet (X1 union X2) is SubSpace of X2 and
A9: 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 by A4,A5,A6;
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
A10: the carrier of X1 union X2 = A1 \/ A2 by Def2;
A11: the carrier of Y1 union Y2 = C1 \/ C2 by Def2;
now
assume Y1 misses (X1 union X2);
then
A12: C1 misses (A1 \/ A2) by A10;
A13: now
per cases;
suppose
X1 union X2 is SubSpace of Y1 union Y2;
then A1 \/ A2 c= C1 \/ C2 by A10,A11,Th4;
then
A14: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ (C2 /\ (A1 \/ A2)) by A12,XBOOLE_0:def 7
.= C2 /\ (A1 \/ A2);
then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A10;
then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A10
,Def4;
hence A1 \/ A2 c= A2 by A8,A14,Th4;
end;
suppose
not X1 union X2 is SubSpace of Y1 union Y2;
then consider Y being closed non empty SubSpace of X such that
A15: the TopStruct of X = (Y1 union Y2) union Y and
A16: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A9;
reconsider C = the carrier of Y as Subset of X by Th1;
the carrier of X = (C1 \/ C2) \/ C by A11,A15,Def2;
then
A17: A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A12,XBOOLE_0:def 7
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A18: now
assume C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A10;
then
A19: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A10,Def4
;
the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
then
A20: C /\ (A1 \/ A2) c= A1 /\ A2 by A16,A19,Th4;
A21: A1 /\ A2 c= A2 by XBOOLE_1:17;
then
A22: C /\ (A1 \/ A2) c= A2 by A20,XBOOLE_1:1;
now
per cases;
suppose
C2 /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A2 by A17,A20,A21,XBOOLE_1:1;
end;
suppose
C2 /\ (A1 \/ A2) <> {};
then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A10;
then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2
) by A10,Def4;
then C2 /\ (A1 \/ A2) c= A2 by A8,Th4;
hence A1 \/ A2 c= A2 by A17,A22,XBOOLE_1:8;
end;
end;
hence A1 \/ A2 c= A2;
end;
now
assume C2 /\ (A1 \/ A2) <> {};
then C2 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y2 meets (X1 union X2) by A10;
then
A23: the carrier of Y2 meet (X1 union X2) = C2 /\ ( A1 \/ A2) by A10
,Def4;
then
A24: C2 /\ (A1 \/ A2) c= A2 by A8,Th4;
now
per cases;
suppose
C /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A2 by A8,A17,A23,Th4;
end;
suppose
C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A10;
then
A25: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
by A10,Def4;
the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A16,A25,Th4;
then A1 \/ A2 c= A2 \/ A1 /\ A2 by A17,A24,XBOOLE_1:13;
hence A1 \/ A2 c= A2 by XBOOLE_1:12,17;
end;
end;
hence A1 \/ A2 c= A2;
end;
hence A1 \/ A2 c= A2 by A17,A18;
end;
end;
A1 c= A1 \/ A2 by XBOOLE_1:7;
then A1 c= A2 by A13,XBOOLE_1:1;
hence contradiction by A5,Th4;
end;
then
the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A10,Def4;
then
A26: C1 /\ (A1 \/ A2) c= A1 by A7,Th4;
now
assume not Y2 meets (X1 union X2);
then
A27: C2 misses (A1 \/ A2) by A10;
A28: now
per cases;
suppose
X1 union X2 is SubSpace of Y1 union Y2;
then A1 \/ A2 c= C1 \/ C2 by A10,A11,Th4;
then
A29: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ {} by A27,XBOOLE_0:def 7
.= C1 /\ (A1 \/ A2);
then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A10;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A10
,Def4;
hence A1 \/ A2 c= A1 by A7,A29,Th4;
end;
suppose
not X1 union X2 is SubSpace of Y1 union Y2;
then consider Y being closed non empty SubSpace of X such that
A30: the TopStruct of X = (Y1 union Y2) union Y and
A31: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A9;
reconsider C = the carrier of Y as Subset of X by Th1;
the carrier of X = (C1 \/ C2) \/ C by A11,A30,Def2;
then
A32: A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A27,XBOOLE_0:def 7
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
A33: now
assume C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A10;
then
A34: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A10,Def4
;
the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
then
A35: C /\ (A1 \/ A2) c= A1 /\ A2 by A31,A34,Th4;
A36: A1 /\ A2 c= A1 by XBOOLE_1:17;
then
A37: C /\ (A1 \/ A2) c= A1 by A35,XBOOLE_1:1;
now
per cases;
suppose
C1 /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A1 by A32,A35,A36,XBOOLE_1:1;
end;
suppose
C1 /\ (A1 \/ A2) <> {};
then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A10;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2
) by A10,Def4;
then C1 /\ (A1 \/ A2) c= A1 by A7,Th4;
hence A1 \/ A2 c= A1 by A32,A37,XBOOLE_1:8;
end;
end;
hence A1 \/ A2 c= A1;
end;
now
assume C1 /\ (A1 \/ A2) <> {};
then C1 meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y1 meets (X1 union X2) by A10;
then
A38: the carrier of Y1 meet (X1 union X2) = C1 /\ ( A1 \/ A2)
by A10,Def4;
then
A39: C1 /\ (A1 \/ A2) c= A1 by A7,Th4;
now
per cases;
suppose
C /\ (A1 \/ A2) = {};
hence A1 \/ A2 c= A1 by A7,A32,A38,Th4;
end;
suppose
C /\ (A1 \/ A2) <> {};
then C meets (A1 \/ A2) by XBOOLE_0:def 7;
then Y meets (X1 union X2) by A10;
then
A40: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2)
by A10,Def4;
the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A31,A40,Th4;
then A1 \/ A2 c= A1 \/ A1 /\ A2 by A32,A39,XBOOLE_1:13;
hence A1 \/ A2 c= A1 by XBOOLE_1:12,17;
end;
end;
hence A1 \/ A2 c= A1;
end;
hence A1 \/ A2 c= A1 by A32,A33;
end;
end;
A2 c= A1 \/ A2 by XBOOLE_1:7;
then A2 c= A1 by A28,XBOOLE_1:1;
hence contradiction by A6,Th4;
end;
then the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A10,Def4;
then
A41: C2 /\ (A1 \/ A2) c= A2 by A8,Th4;
A42: C1 is open & C2 is open by Th16;
now
per cases;
suppose
A43: A1 \/ A2 c= C1 \/ C2;
thus ex C being Subset of X st the carrier of X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed
proof
take C = (C1 \/ C2)`;
C misses (A1 \/ A2) by A43,SUBSET_1:24;
then C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
hence thesis by A2,A42,PRE_TOPC:2,XBOOLE_1:2;
end;
end;
suppose
A44: not A1 \/ A2 c= C1 \/ C2;
thus ex C being Subset of X st the carrier of X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed
proof
consider Y being closed non empty SubSpace of X such that
A45: the TopStruct of X = (Y1 union Y2) union Y and
A46: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A9,A10,A11,A44
,Th4;
reconsider C = the carrier of Y as Subset of X by Th1;
A47: the carrier of X = (the carrier of Y1 union Y2) \/ C by A45,Def2
.= (C1 \/ C2) \/ C by Def2;
now
assume not Y meets (X1 union X2);
then
A48: C misses (A1 \/ A2) by A10;
the carrier of X = (C1 \/ C2) \/ C by A11,A45,Def2;
then A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by
XBOOLE_1:23
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A48,XBOOLE_0:def 7
.= (C1 \/ C2) /\ (A1 \/ A2);
hence contradiction by A44,XBOOLE_1:17;
end;
then
A49: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A10,Def4;
A50: C is closed by Th11;
the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A46,A49,Th4;
hence thesis by A50,A47;
end;
end;
end;
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 A42,A26,A41,Th58;
hence X1,X2 are_weakly_separated;
end;
hence X1,X2 are_weakly_separated by Th79;
end;
A51: X is SubSpace of X by Th2;
now
assume X1,X2 are_weakly_separated;
then
A52: A1,A2 are_weakly_separated;
now
assume that
A53: not X1 is SubSpace of X2 and
A54: not X2 is SubSpace of X1;
A55: not A2 c= A1 by A54,Th4;
A56: not A1 c= A2 by A53,Th4;
then consider C1, C2 being non empty Subset of X such that
A57: C1 is open and
A58: C2 is open and
A59: C1 /\ (A1 \/ A2) c= A1 and
A60: C2 /\ (A1 \/ A2) c= A2 and
A61: 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
by A52,A55,Th59;
A62: now
assume C2 misses (A1 \/ A2);
then
A63: C2 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
now
per cases;
suppose
A64: A1 \/ A2 c= C1 \/ C2;
A65: A2 c= A1 \/ A2 by XBOOLE_1:7;
A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A64,XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ {} by A63,XBOOLE_1:23
.= C1 /\ (A1 \/ A2);
hence contradiction by A55,A59,A65,XBOOLE_1:1;
end;
suppose
not A1 \/ A2 c= C1 \/ C2;
then consider C being non empty Subset of X such that
C is closed and
A66: C /\ (A1 \/ A2) c= A1 /\ A2 and
A67: the carrier of X = (C1 \/ C2) \/ C by A61;
A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A67,XBOOLE_1:28
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A63,XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
then A1 \/ A2 c= A1 \/ A1 /\ A2 by A59,A66,XBOOLE_1:13;
then
A68: A1 \/ A2 c= A1 by XBOOLE_1:12,17;
A2 c= A1 \/ A2 by XBOOLE_1:7;
hence contradiction by A55,A68,XBOOLE_1:1;
end;
end;
hence contradiction;
end;
A69: now
assume C1 misses (A1 \/ A2);
then
A70: C1 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
now
per cases;
suppose
A71: A1 \/ A2 c= C1 \/ C2;
A72: A1 c= A1 \/ A2 by XBOOLE_1:7;
A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A71,XBOOLE_1:28
.= {} \/ (C2 /\ (A1 \/ A2)) by A70,XBOOLE_1:23
.= C2 /\ (A1 \/ A2);
hence contradiction by A56,A60,A72,XBOOLE_1:1;
end;
suppose
not A1 \/ A2 c= C1 \/ C2;
then consider C being non empty Subset of X such that
C is closed and
A73: C /\ (A1 \/ A2) c= A1 /\ A2 and
A74: the carrier of X = (C1 \/ C2) \/ C by A61;
A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A74,XBOOLE_1:28
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A70,XBOOLE_1:23
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23;
then A1 \/ A2 c= A2 \/ A1 /\ A2 by A60,A73,XBOOLE_1:13;
then
A75: A1 \/ A2 c= A2 by XBOOLE_1:12,17;
A1 c= A1 \/ A2 by XBOOLE_1:7;
hence contradiction by A56,A75,XBOOLE_1:1;
end;
end;
hence contradiction;
end;
thus 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)
proof
consider Y2 being strict open non empty SubSpace of X such that
A76: C2 = the carrier of Y2 by A58,Th20;
A77: the carrier of X1 union X2 = A1 \/ A2 by Def2;
then Y2 meets (X1 union X2) by A62,A76;
then
A78: the carrier of Y2 meet (X1 union X2) = C2 /\ (A1 \/ A2) by A76,A77,Def4
;
consider Y1 being strict open non empty SubSpace of X such that
A79: C1 = the carrier of Y1 by A57,Th20;
A80: the carrier of Y1 union Y2 = C1 \/ C2 by A79,A76,Def2;
A81: now
assume
A82: not X1 union X2 is SubSpace of Y1 union Y2;
then consider C being non empty Subset of X such that
A83: C is closed and
A84: C /\ (A1 \/ A2) c= A1 /\ A2 and
A85: the carrier of X = (C1 \/ C2) \/ C by A61,A77,A80,Th4;
A86: not A1 \/ A2 c= C1 \/ C2 by A77,A80,A82,Th4;
thus 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
proof
consider Y being strict closed non empty SubSpace of X such that
A87: C = the carrier of Y by A83,Th15;
now
assume C misses (A1 \/ A2);
then
A88: C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A85,XBOOLE_1:28
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A88,XBOOLE_1:23
.= (C1 \/ C2) /\ (A1 \/ A2);
hence contradiction by A86,XBOOLE_1:17;
end;
then Y meets (X1 union X2) by A77,A87;
then
A89: the carrier of Y meet (X1 union X2) = C /\ (A1 \/ A2) by A77,A87
,Def4;
take Y;
A90: the carrier of X1 meet X2 = A1 /\ A2 by A1,Def4;
the carrier of X = (the carrier of Y1 union Y2) \/ C by A79,A76,A85
,Def2
.= the carrier of (Y1 union Y2) union Y by A87,Def2;
hence thesis by A51,A84,A89,A90,Th4,Th5;
end;
end;
take Y1,Y2;
Y1 meets (X1 union X2) by A69,A79,A77;
then the carrier of Y1 meet (X1 union X2) = C1 /\ (A1 \/ A2) by A79,A77
,Def4;
hence thesis by A59,A60,A78,A81,Th4;
end;
end;
hence 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);
end;
hence thesis by A3;
end;
theorem
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)))
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume
A1: X = X1 union X2;
then
A2: A1 \/ A2 = the carrier of X by Def2;
assume
A3: X1 meets X2;
A4: now
assume
A5: 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);
now
assume ( not X1 is SubSpace of X2)& not X2 is SubSpace of X1;
then consider Y1, Y2 being open non empty SubSpace of X such that
A6: Y1 is SubSpace of X1 & Y2 is SubSpace of X2 and
A7: 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 by A5;
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
A8: now
per cases;
suppose
A9: A1 \/ A2 = C1 \/ C2;
thus ex C being Subset of X st A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1
/\ A2 & C is closed
proof
take {}X;
thus thesis by A9,XBOOLE_1:2;
end;
end;
suppose
A10: A1 \/ A2 <> C1 \/ C2;
thus ex C being Subset of X st A1 \/ A2 = (C1 \/ C2) \/ C & C c= A1
/\ A2 & C is closed
proof
consider Y being closed non empty SubSpace of X such that
A11: X = (Y1 union Y2) union Y and
A12: Y is SubSpace of X1 meet X2 by A2,A7,A10,Def2;
reconsider C = the carrier of Y as Subset of X by Th1;
A1 /\ A2 = the carrier of X1 meet X2 by A3,Def4;
then
A13: C c= A1 /\ A2 by A12,Th4;
A14: C is closed by Th11;
A1 \/ A2 = (the carrier of Y1 union Y2) \/ C by A2,A11,Def2
.= (C1 \/ C2) \/ C by Def2;
hence thesis by A14,A13;
end;
end;
end;
A15: C1 is open & C2 is open by Th16;
C1 c= A1 & C2 c= A2 by A6,Th4;
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 A2,A15,A8,Th60;
hence X1,X2 are_weakly_separated;
end;
hence X1,X2 are_weakly_separated by Th79;
end;
now
assume X1,X2 are_weakly_separated;
then
A16: A1,A2 are_weakly_separated;
now
assume ( not X1 is SubSpace of X2)& not X2 is SubSpace of X1;
then ( not A1 c= A2)& not A2 c= A1 by Th4;
then consider C1, C2 being non empty Subset of X such that
A17: C1 is open and
A18: C2 is open and
A19: C1 c= A1 & C2 c= A2 and
A20: 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 by A2,A16,Th61;
thus 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)
proof
consider Y2 being strict open non empty SubSpace of X such that
A21: C2 = the carrier of Y2 by A18,Th20;
consider Y1 being strict open non empty SubSpace of X such that
A22: C1 = the carrier of Y1 by A17,Th20;
take Y1,Y2;
now
assume X <> Y1 union Y2;
then consider C being non empty Subset of X such that
A23: A1 \/ A2 = (C1 \/ C2) \/ C and
A24: C c= A1 /\ A2 and
A25: C is closed by A1,A2,A20,A22,A21,Def2;
thus ex Y being closed non empty SubSpace of X st X = (Y1 union Y2)
union Y & Y is SubSpace of X1 meet X2
proof
A26: C c= the carrier of X1 meet X2 by A3,A24,Def4;
consider Y being strict closed non empty SubSpace of X such that
A27: C = the carrier of Y by A25,Th15;
take Y;
the carrier of X = (the carrier of Y1 union Y2) \/ C by A2,A22,A21
,A23,Def2
.= the carrier of (Y1 union Y2) union Y by A27,Def2;
hence thesis by A1,A27,A26,Th4,Th5;
end;
end;
hence thesis by A19,A22,A21,Th4;
end;
end;
hence 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);
end;
hence thesis by A4;
end;
theorem
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)
proof
assume
A1: X = X1 union X2;
assume
A2: X1 misses X2;
thus X1,X2 are_weakly_separated implies X1 is open SubSpace of X & X2 is
open SubSpace of X
proof
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume X1,X2 are_weakly_separated;
then X1,X2 are_separated by A2,Th78;
then
A3: A1,A2 are_separated;
A1 \/ A2 = [#]X by A1,Def2;
then A1 is open & A2 is open by A3,CONNSP_1:4;
hence thesis by Th16;
end;
thus thesis by Th81;
end;
::A Characterization of Separated Subspaces by means of Weakly Separated ones.
theorem
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)
proof
thus X1,X2 are_separated implies 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)
proof
assume X1,X2 are_separated;
then consider Y1, Y2 being open non empty SubSpace of X such that
A1: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 &( Y1 misses Y2 or Y1
meet Y2 misses X1 union X2) by Th77;
take Y1,Y2;
thus thesis by A1,Th81;
end;
given Y1, Y2 being non empty SubSpace of X such that
A2: Y1,Y2 are_weakly_separated and
A3: X1 is SubSpace of Y1 & X2 is SubSpace of Y2 and
A4: Y1 misses Y2 or Y1 meet Y2 misses X1 union X2;
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
now
let A1, A2 be Subset of X such that
A5: A1 = the carrier of X1 & A2 = the carrier of X2;
now
per cases;
suppose
Y1 misses Y2;
then Y1,Y2 are_separated by A2,Th78;
then
A6: C1,C2 are_separated;
A1 c= C1 & A2 c= C2 by A3,A5,Th4;
hence A1,A2 are_separated by A6,CONNSP_1:7;
end;
suppose
A7: not Y1 misses Y2;
ex B1, B2 being Subset of X st B1,B2 are_weakly_separated & A1 c=
B1 & A2 c= B2 & B1 /\ B2 misses A1 \/ A2
proof
take C1,C2;
the carrier of Y1 meet Y2 = C1 /\ C2 & the carrier of X1 union
X2 = A1 \/ A2 by A5,A7,Def2,Def4;
hence thesis by A2,A3,A4,A5,A7,Th4;
end;
hence A1,A2 are_separated by Th62;
end;
end;
hence A1,A2 are_separated;
end;
hence thesis;
end;
theorem :: WAYBEL34:30, AK, 20.02.2006
for T being TopStruct holds T|[#]T = the TopStruct of T
proof
let T be TopStruct;
the TopStruct of T is strict SubSpace of T & the carrier of T = [#]the
TopStruct of T by Th2,PRE_TOPC:10;
hence thesis by PRE_TOPC:def 5;
end;