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;

( 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;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

now :: thesis: not Y1 misses X1 union X2

hence
( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
by A8; :: thesis: verumassume
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;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