let X be non empty non almost_discrete TopSpace; :: thesis: for X1 being non empty closed boundary SubSpace of X ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty closed boundary SubSpace of X; :: thesis: ex X2 being non empty strict open proper dense SubSpace of X st X1,X2 constitute_a_decomposition
consider X2 being non empty strict proper SubSpace of X such that
A1: X1,X2 constitute_a_decomposition by Th8;
reconsider X2 = X2 as non empty strict open proper dense SubSpace of X by A1, Th31, TSEP_2:34;
take X2 ; :: thesis: X1,X2 constitute_a_decomposition
thus X1,X2 constitute_a_decomposition by A1; :: thesis: verum