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 by TSEP_1:def 7;

now

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, TSEP_1:def 3;
then C1 /\ C2 <> {} by XBOOLE_0:def 7;
then A1 /\ A2 <> {} by A1, A5, XBOOLE_1:3, XBOOLE_1:27;
then A1 meets A2 by XBOOLE_0:def 7;
then X1 meets X2 by TSEP_1:def 3;
then A1 /\ A2 = the carrier of (X1 meet X2) by TSEP_1:def 4;
then A1 /\ A2 = C1 /\ C2 by A2, A3, A5, TSEP_1:def 4;
hence C1,C2 are_weakly_separated by A1, A4, A5, Th25; :: thesis: verum

end;

hence Y1,Y2 are_weakly_separated by TSEP_1:def 7; :: thesis: verum