for X being non empty non almost_discrete TopSpace
for X0 being non empty nowhere_dense SubSpace of X holds
( ( X0 is boundary & X0 is closed ) or ex X1 being non empty strict proper everywhere_dense SubSpace of X ex X2 being non empty strict closed boundary SubSpace of X st
( X1 meet X2 = TopStruct(# the carrier of X0, the topology of X0 #) & X1 union X2 = TopStruct(# the carrier of X, the topology of X #) ) )