let X be non empty non almost_discrete TopSpace; for X0 being non empty nowhere_dense SubSpace of X holds
( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )
let X0 be non empty nowhere_dense SubSpace of X; ( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
A1:
X is SubSpace of X
by TSEP_1:2;
D is nowhere_dense
by Th35;
then consider C, B being Subset of X such that
A2:
( C is closed & C is boundary )
and
A3:
B is everywhere_dense
and
A4:
C /\ B = D
and
A5:
C \/ B = the carrier of X
by TOPS_3:51;
B <> {}
by A4;
then consider X1 being non empty strict everywhere_dense SubSpace of X such that
A6:
B = the carrier of X1
by A3, Th17;
assume A7:
( not X0 is boundary or not X0 is closed )
; ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) )
then reconsider X1 = X1 as non empty strict proper everywhere_dense SubSpace of X by A6, TEX_2:8;
C <> {}
by A4;
then consider X2 being non empty strict closed boundary SubSpace of X such that
A8:
C = the carrier of X2
by A2, Th67;
take
X1
; ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) )
take
X2
; ( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) )
C meets B
by A4, XBOOLE_0:def 7;
then
X1 meets X2
by A8, A6, TSEP_1:def 3;
then
the carrier of (X1 meet X2) = D
by A4, A8, A6, TSEP_1:def 4;
hence
X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #)
by TSEP_1:5; X1 union X2 = TopStruct(# the carrier of X, the topology of X #)
the carrier of (X1 union X2) = the carrier of X
by A5, A8, A6, TSEP_1:def 2;
hence
X1 union X2 = TopStruct(# the carrier of X, the topology of X #)
by A1, TSEP_1:5; verum