let X be non empty TopSpace; :: thesis: for X0, X1, X2, Y1, Y2 being non empty SubSpace of X st X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union X2 is not SubSpace of Y1 union Y2 & TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & X0 meet (X1 union X2) is SubSpace of X1 meet X2 holds
( Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2 )
let X0, X1, X2, Y1, Y2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union X2 is not SubSpace of Y1 union Y2 & TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & X0 meet (X1 union X2) is SubSpace of X1 meet X2 implies ( Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2 ) )
assume A1: X1 meets X2 ; :: thesis: ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or X1 union X2 is SubSpace of Y1 union Y2 or not TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 or not Y1 meet (X1 union X2) is SubSpace of X1 or not Y2 meet (X1 union X2) is SubSpace of X2 or not X0 meet (X1 union X2) is SubSpace of X1 meet X2 or ( Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2 ) )
assume A2: ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 ) ; :: thesis: ( X1 union X2 is SubSpace of Y1 union Y2 or not TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 or not Y1 meet (X1 union X2) is SubSpace of X1 or not Y2 meet (X1 union X2) is SubSpace of X2 or not X0 meet (X1 union X2) is SubSpace of X1 meet X2 or ( Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2 ) )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
reconsider C2 = the carrier of Y2 as Subset of X by TSEP_1:1;
reconsider C1 = the carrier of Y1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
A3: the carrier of (Y1 union Y2) = C1 \/ C2 by TSEP_1:def 2;
A4: Y1 is SubSpace of Y1 union Y2 by TSEP_1:22;
assume A5: X1 union X2 is not SubSpace of Y1 union Y2 ; :: thesis: ( not TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 or not Y1 meet (X1 union X2) is SubSpace of X1 or not Y2 meet (X1 union X2) is SubSpace of X2 or not X0 meet (X1 union X2) is SubSpace of X1 meet X2 or ( Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2 ) )
assume A6: TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 ; :: thesis: ( not Y1 meet (X1 union X2) is SubSpace of X1 or not Y2 meet (X1 union X2) is SubSpace of X2 or not X0 meet (X1 union X2) is SubSpace of X1 meet X2 or ( Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2 ) )
assume A7: ( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 ) ; :: thesis: ( not X0 meet (X1 union X2) is SubSpace of X1 meet X2 or ( Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2 ) )
assume X0 meet (X1 union X2) is SubSpace of X1 meet X2 ; :: thesis: ( Y1 union Y2 meets X1 union X2 & X0 meets X1 union X2 )
then Y1 meets X1 union X2 by A1, A2, A6, A7, Th32;
hence Y1 union Y2 meets X1 union X2 by A4, Th18; :: thesis: X0 meets X1 union X2
A8: the carrier of (X1 union X2) = A1 \/ A2 by TSEP_1:def 2;
then A9: not A1 \/ A2 c= C1 \/ C2 by A5, A3, TSEP_1:4;
now :: thesis: not X0 misses X1 union X2
assume X0 misses X1 union X2 ; :: thesis: contradiction
then A10: C misses A1 \/ A2 by A8, TSEP_1:def 3;
the carrier of X = (C1 \/ C2) \/ C by A6, A3, TSEP_1:def 2;
then A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23
.= (C1 \/ C2) /\ (A1 \/ A2) by A10 ;
hence contradiction by A9, XBOOLE_1:17; :: thesis: verum
end;
hence X0 meets X1 union X2 ; :: thesis: verum