let X be non empty non almost_discrete TopSpace; :: thesis: for X0 being non empty nowhere_dense SubSpace of X ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
let X0 be non empty nowhere_dense SubSpace of X; :: thesis: ex X1 being non empty strict open proper dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
reconsider D = the carrier of X0 as non empty Subset of X by TSEP_1:1;
D is nowhere_dense by Th35;
then consider C, B being Subset of X such that
A1: ( C is closed & C is boundary ) and
A2: ( B is open & B is dense ) and
A3: C /\ (D \/ B) = D and
A4: C misses B and
A5: C \/ B = the carrier of X by TOPS_3:52;
B <> {} by A2, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A6: B = the carrier of X1 by A2, Th23;
A7: C <> {} by A3;
then consider X2 being non empty strict closed boundary SubSpace of X such that
A8: C = the carrier of X2 by A1, Th67;
A9: C /\ B = {} by A4, XBOOLE_0:def 7;

now :: thesis: B is proper

assume not B is proper ; :: thesis: contradiction
then B = the carrier of X by SUBSET_1:def 6;
hence contradiction by A7, A9, XBOOLE_1:28; :: thesis: verum

end;

then reconsider X1 = X1 as non empty strict open proper dense SubSpace of X by A6, TEX_2:8;
take X1 ; :: thesis: ex X2 being non empty strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
take X2 ; :: thesis: ( X1,X2 constitute_a_decomposition & X0 is SubSpace of X2 )
for P, Q being Subset of X st P = the carrier of X1 & Q = the carrier of X2 holds
P,Q constitute_a_decomposition by A4, A5, A6, A8;
hence X1,X2 constitute_a_decomposition ; :: thesis: X0 is SubSpace of X2
D c= C by A3, XBOOLE_1:17;
hence X0 is SubSpace of X2 by A8, TSEP_1:4; :: thesis: verum