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 ;

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

hence
X1,X2 are_weakly_separated
; :: thesis: verumA1,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;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