for X being non empty TopSpace
for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds
( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 )