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 )
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 A1: 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 ) )
then ( X0 meets X1 & X1 is SubSpace of X1 union X2 ) by Th22, TSEP_1:22;
then A2: X0 meets X1 union X2 by Th23;
reconsider S = TopStruct(# the carrier of X1,the topology of X1 #) as SubSpace of X by Th11;
assume X0 misses X2 ; :: thesis: ( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 )
then X0 meet (X1 union X2) = TopStruct(# the carrier of X1,the topology of X1 #) by A1, Th33;
then ( S is closed SubSpace of X1 union X2 & X1 union X2 = X2 union X1 ) by A2, Th43;
hence ( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 ) by Th13; :: thesis: verum