for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X st X = X1 union X2 & X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty closed SubSpace of X st
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & ( X = Y1 union Y2 or ex Y being non empty open SubSpace of X st
( X = (Y1 union Y2) union Y & Y is SubSpace of X1 meet X2 ) ) ) ) )