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 that
A1: X1 is not SubSpace of X2 and
A2: 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 ) )
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;
assume A3: 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 that
A4: Y1 meet (X1 union X2) is SubSpace of X1 and
A5: Y2 meet (X1 union X2) is SubSpace of X2 ; :: thesis: ( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
A6: the carrier of (X1 union X2) = A1 \/ A2 by TSEP_1:def 2;
A7: the carrier of (Y1 union Y2) = C1 \/ C2 by TSEP_1:def 2;
A8: now :: thesis: not Y2 misses X1 union X2
assume Y2 misses X1 union X2 ; :: thesis: contradiction
then A9: C2 misses A1 \/ A2 by A6, TSEP_1:def 3;
A1 \/ A2 c= C1 \/ C2 by A3, A6, A7, TSEP_1:4;
then A10: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
.= C1 /\ (A1 \/ A2) by A9 ;
then C1 meets A1 \/ A2 ;
then Y1 meets X1 union X2 by A6, TSEP_1:def 3;
then the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A6, TSEP_1:def 4;
then A11: A1 \/ A2 c= A1 by A4, A10, TSEP_1:4;
A2 c= A1 \/ A2 by XBOOLE_1:7;
hence contradiction by A2, TSEP_1:4, A11, XBOOLE_1:1; :: thesis: verum
end;
now :: thesis: not Y1 misses X1 union X2
assume Y1 misses X1 union X2 ; :: thesis: contradiction
then A12: C1 misses A1 \/ A2 by A6, TSEP_1:def 3;
A1 \/ A2 c= C1 \/ C2 by A3, A6, A7, TSEP_1:4;
then A13: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
.= C2 /\ (A1 \/ A2) by A12 ;
then C2 meets A1 \/ A2 ;
then Y2 meets X1 union X2 by A6, TSEP_1:def 3;
then the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A6, TSEP_1:def 4;
then A14: A1 \/ A2 c= A2 by A5, A13, TSEP_1:4;
A1 c= A1 \/ A2 by XBOOLE_1:7;
then A1 c= A2 by A14, 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 A8; :: thesis: verum