let X be non empty non almost_discrete TopSpace; :: thesis: for X0 being proper everywhere_dense SubSpace of X ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
let X0 be proper everywhere_dense SubSpace of X; :: thesis: ex X1 being strict open proper dense SubSpace of X ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
D is everywhere_dense by Th16;
then consider C, B being Subset of X such that
A1: ( C is open & C is dense ) and
A2: ( B is closed & B is boundary ) and
A3: C \/ (D /\ B) = D and
A4: C misses B and
A5: C \/ B = the carrier of X by TOPS_3:50;
C <> {} by A1, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A6: C = the carrier of X1 by A1, Th23;
then not B is empty by A5, SUBSET_1:def 6;
then consider X2 being non empty strict closed boundary SubSpace of X such that
A8: B = the carrier of X2 by A2, Th67;
reconsider X1 = X1 as strict open proper dense SubSpace of X by A6, A7, TEX_2:8;
take X1 ; :: thesis: ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
take X2 ; :: thesis: ( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
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: X1 is SubSpace of X0
C c= D by A3, XBOOLE_1:7;
hence X1 is SubSpace of X0 by A6, TSEP_1:4; :: thesis: verum