let X be non empty TopSpace; :: thesis: for X2, X1, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of X2 & Y2 is SubSpace of X1 & X1,X2 are_weakly_separated holds
( X1 union Y1,X2 union Y2 are_weakly_separated & Y1 union X1,Y2 union X2 are_weakly_separated )
let X2, X1 be non empty SubSpace of X; :: thesis: for Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of X2 & Y2 is SubSpace of X1 & X1,X2 are_weakly_separated holds
( X1 union Y1,X2 union Y2 are_weakly_separated & Y1 union X1,Y2 union X2 are_weakly_separated )
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
let Y1, Y2 be non empty SubSpace of X; :: thesis: ( Y1 is SubSpace of X2 & Y2 is SubSpace of X1 & X1,X2 are_weakly_separated implies ( X1 union Y1,X2 union Y2 are_weakly_separated & Y1 union X1,Y2 union X2 are_weakly_separated ) )
assume A1: ( Y1 is SubSpace of X2 & Y2 is SubSpace of X1 ) ; :: thesis: ( not X1,X2 are_weakly_separated or ( X1 union Y1,X2 union Y2 are_weakly_separated & Y1 union X1,Y2 union X2 are_weakly_separated ) )
reconsider B2 = the carrier of Y2 as Subset of X by Th1;
reconsider B1 = the carrier of Y1 as Subset of X by Th1;
assume X1,X2 are_weakly_separated ; :: thesis: ( X1 union Y1,X2 union Y2 are_weakly_separated & Y1 union X1,Y2 union X2 are_weakly_separated )
then A2: A1,A2 are_weakly_separated by Def9;
A3: ( B1 c= A2 & B2 c= A1 ) by A1, Th4;

A4: now

let D1, D2 be Subset of X; :: thesis: ( D1 = the carrier of (X1 union Y1) & D2 = the carrier of (X2 union Y2) implies D1,D2 are_weakly_separated )
assume ( D1 = the carrier of (X1 union Y1) & D2 = the carrier of (X2 union Y2) ) ; :: thesis: D1,D2 are_weakly_separated
then ( A1 \/ B1 = D1 & A2 \/ B2 = D2 ) by Def2;
hence D1,D2 are_weakly_separated by A3, A2, Th56; :: thesis: verum

end;

hence X1 union Y1,X2 union Y2 are_weakly_separated by Def9; :: thesis: Y1 union X1,Y2 union X2 are_weakly_separated
thus Y1 union X1,Y2 union X2 are_weakly_separated by A4, Def9; :: thesis: verum