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

now :: thesis: for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated

let A1, A2 be Subset of X; :: thesis: ( A1 = the carrier of X1 & A2 = the carrier of X2 implies A1,A2 are_weakly_separated )
assume A4: ( A1 = the carrier of X1 & A2 = the carrier of X2 ) ; :: thesis: A1,A2 are_weakly_separated
then A1 \/ A2 = the carrier of (X1 union X2) by TSEP_1:def 2;
then A1 \/ A2 = C1 \/ C2 by A2, TSEP_1:def 2;
hence A1,A2 are_weakly_separated by A1, A3, A4, Th22; :: thesis: verum

end;

hence X1,X2 are_weakly_separated ; :: thesis: verum