let X be non empty non almost_discrete TopSpace; :: thesis: 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; :: thesis: ( ( 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 ) ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum