let X be non empty TopSpace; for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open 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 non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) )
let X1, X2 be non empty SubSpace of X; ( 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 non empty open 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 non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet 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;
assume A1:
X1 meets X2
; ( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open 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 non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) )
A2:
[#] X = the carrier of X
;
A3:
now ( ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open 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 non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) implies X1,X2 are_weakly_separated )assume A4:
(
X1 is
SubSpace of
X2 or
X2 is
SubSpace of
X1 or ex
Y1,
Y2 being non
empty open 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 non
empty closed SubSpace of
X st
(
TopStruct(# the
carrier of
X, the
topology of
X #)
= (Y1 union Y2) union Y &
Y meet (X1 union X2) is
SubSpace of
X1 meet X2 ) ) ) )
;
X1,X2 are_weakly_separated now ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 implies X1,X2 are_weakly_separated )assume that A5:
X1 is not
SubSpace of
X2
and A6:
X2 is not
SubSpace of
X1
;
X1,X2 are_weakly_separated consider Y1,
Y2 being non
empty open 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 non
empty closed SubSpace of
X st
(
TopStruct(# the
carrier of
X, the
topology 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;
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;
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 ex C being Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed )per cases
( A1 \/ A2 c= C1 \/ C2 or not A1 \/ A2 c= C1 \/ C2 )
;
suppose A44:
not
A1 \/ A2 c= C1 \/ C2
;
ex C being Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed )thus
ex
C being
Subset of
X st
( the
carrier of
X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 &
C is
closed )
verumproof
consider Y being non
empty closed SubSpace of
X such that A45:
TopStruct(# the
carrier of
X, the
topology 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
;
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
ex
C being
Subset of
X st
( the
carrier of
X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 &
C is
closed )
by A50, A47;
verum
end; end; end; end; then
for
A1,
A2 being
Subset of
X st
A1 = the
carrier of
X1 &
A2 = the
carrier of
X2 holds
A1,
A2 are_weakly_separated
by A42, A26, A41, Th58;
hence
X1,
X2 are_weakly_separated
;
verum end; hence
X1,
X2 are_weakly_separated
by Th79;
verum end;
A51:
X is SubSpace of X
by Th2;
now ( not X1,X2 are_weakly_separated or X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open 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 non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) )assume
X1,
X2 are_weakly_separated
;
( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open 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 non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) )then A52:
A1,
A2 are_weakly_separated
;
now ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 implies ex Y1, Y2 being non empty open 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 non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) )assume that A53:
X1 is not
SubSpace of
X2
and A54:
X2 is not
SubSpace of
X1
;
ex Y1, Y2 being non empty open 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 non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) )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;
thus
ex
Y1,
Y2 being non
empty open 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 non
empty closed SubSpace of
X st
(
TopStruct(# the
carrier of
X, the
topology of
X #)
= (Y1 union Y2) union Y &
Y meet (X1 union X2) is
SubSpace of
X1 meet X2 ) ) )
verumproof
consider Y2 being non
empty strict open 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 non
empty strict open 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 ( X1 union X2 is not SubSpace of Y1 union Y2 implies ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) )assume A82:
X1 union X2 is not
SubSpace of
Y1 union Y2
;
ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 )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 non
empty closed SubSpace of
X st
(
TopStruct(# the
carrier of
X, the
topology of
X #)
= (Y1 union Y2) union Y &
Y meet (X1 union X2) is
SubSpace of
X1 meet X2 )
verumproof
consider Y being non
empty strict closed SubSpace of
X such that A87:
C = the
carrier of
Y
by A83, Th15;
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
;
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 )
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
(
TopStruct(# the
carrier of
X, the
topology of
X #)
= (Y1 union Y2) union Y &
Y meet (X1 union X2) is
SubSpace of
X1 meet X2 )
by A51, A84, A89, A90, Th4, Th5;
verum
end; end;
take
Y1
;
ex Y2 being non empty open 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 non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) )
take
Y2
;
( 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 non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) )
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
(
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 non
empty closed SubSpace of
X st
(
TopStruct(# the
carrier of
X, the
topology of
X #)
= (Y1 union Y2) union Y &
Y meet (X1 union X2) is
SubSpace of
X1 meet X2 ) ) )
by A59, A60, A78, A81, Th4;
verum
end; end; hence
(
X1 is
SubSpace of
X2 or
X2 is
SubSpace of
X1 or ex
Y1,
Y2 being non
empty open 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 non
empty closed SubSpace of
X st
(
TopStruct(# the
carrier of
X, the
topology of
X #)
= (Y1 union Y2) union Y &
Y meet (X1 union X2) is
SubSpace of
X1 meet X2 ) ) ) )
;
verum end;
hence
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open 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 non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) )
by A3; verum