theorem :: TEX_3:54

for X being non empty non discrete TopSpace
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