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 A2, Th28;

X0 meets X1 by A2, Th17;

then X0 meets X1 union X2 by A1, Th18;

then S is closed SubSpace of X1 union X2 by A3, Th38;

hence ( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 ) by Th8; :: thesis: verum

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 A2, Th28;

X0 meets X1 by A2, Th17;

then X0 meets X1 union X2 by A1, Th18;

then S is closed SubSpace of X1 union X2 by A3, Th38;

hence ( X1 is closed SubSpace of X1 union X2 & X1 is closed SubSpace of X2 union X1 ) by Th8; :: thesis: verum