let X be non empty non almost_discrete TopSpace; 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; 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
; ex X2 being strict closed boundary SubSpace of X st
( X1,X2 constitute_a_decomposition & X1 is SubSpace of X0 )
take
X2
; ( 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
; X1 is SubSpace of X0
C c= D
by A3, XBOOLE_1:7;
hence
X1 is SubSpace of X0
by A6, TSEP_1:4; verum