let X be non empty non discrete TopSpace; :: thesis: for X1 being non empty proper dense SubSpace of X ex X2 being non empty strict boundary SubSpace of X st X1,X2 constitute_a_decomposition
let X1 be non empty proper dense SubSpace of X; :: thesis: ex X2 being non empty strict boundary 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 boundary SubSpace of X by A1, Th31;
take X2 ; :: thesis: X1,X2 constitute_a_decomposition
thus X1,X2 constitute_a_decomposition by A1; :: thesis: verum