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 & X1 misses X2 & Y1,Y2 are_weakly_separated holds
X1,X2 are_separated by Th37, TSEP_1:78;