let X be non empty TopSpace; :: thesis: for X1, X2, Y1, Y2 being non empty SubSpace of X st X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union X2 is SubSpace of Y1 union Y2 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 holds
( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
let X1, X2, Y1, Y2 be non empty SubSpace of X; :: thesis: ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union X2 is SubSpace of Y1 union Y2 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 implies ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume A1: ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 ) ; :: thesis: ( not X1 union X2 is SubSpace of Y1 union Y2 or not Y1 meet (X1 union X2) is SubSpace of X1 or not Y2 meet (X1 union X2) is SubSpace of X2 or ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume A2: X1 union X2 is SubSpace of Y1 union Y2 ; :: thesis: ( not Y1 meet (X1 union X2) is SubSpace of X1 or not Y2 meet (X1 union X2) is SubSpace of X2 or ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume A3: ( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 ) ; :: thesis: ( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
reconsider A1 = the carrier of X1, A2 = the carrier of X2, C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by TSEP_1:1;
A4: ( the carrier of (X1 union X2) = A1 \/ A2 & the carrier of (Y1 union Y2) = C1 \/ C2 ) by TSEP_1:def 2;

A5: now

assume Y1 misses X1 union X2 ; :: thesis: contradiction
then A6: C1 misses A1 \/ A2 by A4, TSEP_1:def 3;
A1 \/ A2 c= C1 \/ C2 by A2, A4, TSEP_1:4;
then A7: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ (C2 /\ (A1 \/ A2)) by A6, XBOOLE_0:def 7
.= C2 /\ (A1 \/ A2) ;
C2 meets A1 \/ A2 by A7, XBOOLE_0:def 7;
then Y2 meets X1 union X2 by A4, TSEP_1:def 3;
then the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A4, TSEP_1:def 5;
then ( A1 \/ A2 c= A2 & A1 c= A1 \/ A2 ) by A3, A7, TSEP_1:4, XBOOLE_1:7;
then A1 c= A2 by XBOOLE_1:1;
hence contradiction by A1, TSEP_1:4; :: thesis: verum

end;

now

assume Y2 misses X1 union X2 ; :: thesis: contradiction
then A8: C2 misses A1 \/ A2 by A4, TSEP_1:def 3;
A1 \/ A2 c= C1 \/ C2 by A2, A4, TSEP_1:4;
then A9: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ {} by A8, XBOOLE_0:def 7
.= C1 /\ (A1 \/ A2) ;
C1 meets A1 \/ A2 by A9, XBOOLE_0:def 7;
then Y1 meets X1 union X2 by A4, TSEP_1:def 3;
then the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A4, TSEP_1:def 5;
then ( A1 \/ A2 c= A1 & A2 c= A1 \/ A2 ) by A3, A9, TSEP_1:4, XBOOLE_1:7;
then A2 c= A1 by XBOOLE_1:1;
hence contradiction by A1, TSEP_1:4; :: thesis: verum

end;

hence ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) by A5; :: thesis: verum