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 closed 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 open 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 closed 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 open 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 closed 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 open 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:
now ( ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty closed 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 open 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 A3:
(
X1 is
SubSpace of
X2 or
X2 is
SubSpace of
X1 or ex
Y1,
Y2 being non
empty closed 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 open 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 A4:
X1 is not
SubSpace of
X2
and A5:
X2 is not
SubSpace of
X1
;
X1,X2 are_weakly_separated consider Y1,
Y2 being non
empty closed 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 non
empty open 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, 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;
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;
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 ex C being Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is open )per cases
( A1 \/ A2 c= C1 \/ C2 or not A1 \/ A2 c= C1 \/ C2 )
;
suppose A43:
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 open )thus
ex
C being
Subset of
X st
( the
carrier of
X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 &
C is
open )
verumproof
consider Y being non
empty open SubSpace of
X such that A44:
TopStruct(# the
carrier of
X, the
topology 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
;
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
ex
C being
Subset of
X st
( the
carrier of
X = (C1 \/ C2) \/ C &
C /\ (A1 \/ A2) c= A1 /\ A2 &
C is
open )
by A49, A46;
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 A41, A25, A40, Th54;
hence
X1,
X2 are_weakly_separated
;
verum end; hence
X1,
X2 are_weakly_separated
by Th79;
verum end;
A50:
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 closed 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 open 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 closed 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 open 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 A51:
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 closed 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 open 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 A52:
X1 is not
SubSpace of
X2
and A53:
X2 is not
SubSpace of
X1
;
ex Y1, Y2 being non empty closed 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 open 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 ) ) )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;
thus
ex
Y1,
Y2 being non
empty closed 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 open 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 closed 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 non
empty strict closed 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 ( X1 union X2 is not SubSpace of Y1 union Y2 implies ex Y being non empty open 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 A81:
X1 union X2 is not
SubSpace of
Y1 union Y2
;
ex Y being non empty open 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 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 non
empty open 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 open SubSpace of
X such that A86:
C = the
carrier of
Y
by A82, Th20;
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
;
( 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 )
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
(
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 A50, A83, A88, A89, Th4, Th5;
verum
end; end;
take
Y1
;
ex Y2 being non empty closed 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 open 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 open 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 A68, A78, A76;
then
the
carrier of
(Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2)
by A78, A76, 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 open 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 A58, A59, A77, A80, Th4;
verum
end; end; hence
(
X1 is
SubSpace of
X2 or
X2 is
SubSpace of
X1 or ex
Y1,
Y2 being non
empty closed 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 open 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 closed 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 open 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 A2; verum