let X be non empty TopSpace; for X1, X2 being non empty SubSpace of X st X = X1 union X2 & 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 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) )
let X1, X2 be non empty SubSpace of X; ( 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 non empty closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y 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:
X = X1 union X2
; ( not X1 meets X2 or ( 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 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) ) )
then A2:
A1 \/ A2 = the carrier of X
by Def2;
assume A3:
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 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) )
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 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y 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 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) )then A16:
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 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) )assume
(
X1 is not
SubSpace of
X2 &
X2 is not
SubSpace of
X1 )
;
ex Y1, Y2 being non empty closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) )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 non
empty closed SubSpace of
X st
(
Y1 is
SubSpace of
X1 &
Y2 is
SubSpace of
X2 & (
X = Y1 union Y2 or ex
Y being non
empty open SubSpace of
X st
(
X = (Y1 union Y2) union Y &
Y is
SubSpace of
X1 meet X2 ) ) )
verumproof
consider Y2 being non
empty strict closed SubSpace of
X such that A21:
C2 = the
carrier of
Y2
by A18, Th15;
consider Y1 being non
empty strict closed SubSpace of
X such that A22:
C1 = the
carrier of
Y1
by A17, Th15;
take
Y1
;
ex Y2 being non empty closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) )
take
Y2
;
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) )
now ( X <> Y1 union Y2 implies ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) )assume
X <> Y1 union Y2
;
ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 )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 non
empty open SubSpace of
X st
(
X = (Y1 union Y2) union Y &
Y is
SubSpace of
X1 meet X2 )
verumproof
A26:
C c= the
carrier of
(X1 meet X2)
by A3, A24, Def4;
consider Y being non
empty strict open SubSpace of
X such that A27:
C = the
carrier of
Y
by A25, Th20;
take
Y
;
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 )
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
(
X = (Y1 union Y2) union Y &
Y is
SubSpace of
X1 meet X2 )
by A1, A27, A26, Th4, Th5;
verum
end; end;
hence
(
Y1 is
SubSpace of
X1 &
Y2 is
SubSpace of
X2 & (
X = Y1 union Y2 or ex
Y being non
empty open SubSpace of
X st
(
X = (Y1 union Y2) union Y &
Y is
SubSpace of
X1 meet X2 ) ) )
by A19, A22, A21, 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 is
SubSpace of
X1 &
Y2 is
SubSpace of
X2 & (
X = Y1 union Y2 or ex
Y being non
empty open SubSpace of
X st
(
X = (Y1 union Y2) union Y &
Y 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 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) )
by A4; verum