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 meets Y2 & Y1 meet Y2 = X1 meet X2 & X1,X2 are_weakly_separated holds
Y1,Y2 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 meets Y2 & Y1 meet Y2 = X1 meet X2 & X1,X2 are_weakly_separated implies Y1,Y2 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 meets Y2 or not Y1 meet Y2 = X1 meet X2 or not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
then A1: ( C1 c= A1 & C2 c= A2 ) by TSEP_1:4;
assume A2: Y1 meets Y2 ; :: thesis: ( not Y1 meet Y2 = X1 meet X2 or not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
assume A3: Y1 meet Y2 = X1 meet X2 ; :: thesis: ( not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
assume X1,X2 are_weakly_separated ; :: thesis: Y1,Y2 are_weakly_separated
then A4: A1,A2 are_weakly_separated ;
now :: thesis: for C1, C2 being Subset of X st C1 = the carrier of Y1 & C2 = the carrier of Y2 holds
C1,C2 are_weakly_separated
let C1, C2 be Subset of X; :: thesis: ( C1 = the carrier of Y1 & C2 = the carrier of Y2 implies C1,C2 are_weakly_separated )
assume A5: ( C1 = the carrier of Y1 & C2 = the carrier of Y2 ) ; :: thesis: C1,C2 are_weakly_separated
then C1 meets C2 by A2;
then C1 /\ C2 <> {} ;
then A1 /\ A2 <> {} by ;
then A1 meets A2 ;
then X1 meets X2 ;
then A1 /\ A2 = the carrier of (X1 meet X2) by TSEP_1:def 4;
then A1 /\ A2 = C1 /\ C2 by ;
hence C1,C2 are_weakly_separated by A1, A4, A5, Th24; :: thesis: verum
end;
hence Y1,Y2 are_weakly_separated ; :: thesis: verum