theorem :: TMAP_1:40

for X being non empty TopSpace
for X1, X2 being non empty SubSpace of X
for X0 being non empty closed SubSpace of X st X1 is SubSpace of X0 & X0 misses X2 holds
( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 )