for X being non empty TopSpace
for Y1, Y2 being non empty SubSpace of X st Y1,Y2 constitute_a_decomposition holds
( Y1 is proper & Y2 is proper )