let X be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X
for X0 being non empty open SubSpace of X st X1 is SubSpace of X0 & X0 misses X2 holds
( X1 is open SubSpace of X1 union X2 & X1 is open SubSpace of X2 union X1 )
let X1, X2 be non empty SubSpace of X; :: thesis: for X0 being non empty open SubSpace of X st X1 is SubSpace of X0 & X0 misses X2 holds
( X1 is open SubSpace of X1 union X2 & X1 is open 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 open SubSpace of X; :: thesis: ( X1 is SubSpace of X0 & X0 misses X2 implies ( X1 is open SubSpace of X1 union X2 & X1 is open SubSpace of X2 union X1 ) )
assume A2: X1 is SubSpace of X0 ; :: thesis: ( not X0 misses X2 or ( X1 is open SubSpace of X1 union X2 & X1 is open SubSpace of X2 union X1 ) )
assume X0 misses X2 ; :: thesis: ( X1 is open SubSpace of X1 union X2 & X1 is open 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 open SubSpace of X1 union X2 by A3, Th39;
hence ( X1 is open SubSpace of X1 union X2 & X1 is open SubSpace of X2 union X1 ) by Th9; :: thesis: verum