let X be non empty TopSpace; :: thesis: 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 )

let X1, X2 be non empty SubSpace of X; :: thesis: 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 )

A1: X1 is SubSpace of X1 union X2 by TSEP_1:22;
reconsider S = TopStruct(# the carrier of X1, the topology of X1 #) as SubSpace of X by Th6;
let X0 be non empty closed SubSpace of X; :: thesis: ( X1 is SubSpace of X0 & X0 misses X2 implies ( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 ) )
assume A2: X1 is SubSpace of X0 ; :: thesis: ( not X0 misses X2 or ( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 ) )
assume X0 misses X2 ; :: thesis: ( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 )
then A3: X0 meet (X1 union X2) = TopStruct(# the carrier of X1, the topology of X1 #) by ;
X0 meets X1 by ;
then X0 meets X1 union X2 by ;
then S is closed SubSpace of X1 union X2 by ;
hence ( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 ) by Th8; :: thesis: verum