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 ;

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

hence
Y1,Y2 are_weakly_separated
; :: thesis: verumC1,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 A1, A5, XBOOLE_1:3, XBOOLE_1:27;

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 A2, A3, A5, TSEP_1:def 4;

hence C1,C2 are_weakly_separated by A1, A4, A5, Th24; :: thesis: verum

end;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 A1, A5, XBOOLE_1:3, XBOOLE_1:27;

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 A2, A3, A5, TSEP_1:def 4;

hence C1,C2 are_weakly_separated by A1, A4, A5, Th24; :: thesis: verum