let X be non empty TopSpace; :: thesis: for X1, X2, 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 X1, X2 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 ;
A3: ( B1 c= A2 & B2 c= A1 ) by A1, Th4;
hence X1 union Y1,X2 union Y2 are_weakly_separated ; :: thesis: Y1 union X1,Y2 union X2 are_weakly_separated
thus Y1 union X1,Y2 union X2 are_weakly_separated by A4; :: thesis: verum