let X be non empty TopSpace; :: thesis: for X1, X2, Y1, Y2, X0 being non empty SubSpace of X st X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & 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 meets X1 union X2 & Y2 meets X1 union X2 )
let X1, X2, Y1, Y2, X0 be non empty SubSpace of X; :: thesis: ( X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & 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 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume A1: X1 meets X2 ; :: thesis: ( X1 is SubSpace of X2 or X2 is SubSpace of X1 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 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume A2: ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 ) ; :: 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 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume A3: 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 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume A4: ( 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 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume A5: X0 meet (X1 union X2) is SubSpace of X1 meet X2 ; :: thesis: ( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider C1 = the carrier of Y1 as Subset of X by TSEP_1:1;
reconsider C2 = the carrier of Y2 as Subset of X by TSEP_1:1;
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
A6: ( the carrier of (X1 union X2) = A1 \/ A2 & the carrier of (Y1 union Y2) = C1 \/ C2 ) by TSEP_1:def 2;

A7: now

assume Y1 misses X1 union X2 ; :: thesis: contradiction
then A8: C1 misses A1 \/ A2 by A6, TSEP_1:def 3;
the carrier of X = (C1 \/ C2) \/ C by A3, A6, TSEP_1:def 2;
then A9: A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A8, XBOOLE_0:def 7
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23 ;

A10: now

assume C2 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2
then C2 meets A1 \/ A2 by XBOOLE_0:def 7;
then Y2 meets X1 union X2 by A6, TSEP_1:def 3;
then A11: the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A6, TSEP_1:def 5;
then A12: C2 /\ (A1 \/ A2) c= A2 by A4, TSEP_1:4;

now

per cases ( C /\ (A1 \/ A2) = {} or C /\ (A1 \/ A2) <> {} ) ;

suppose C /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A2

hence A1 \/ A2 c= A2 by A4, A9, A11, TSEP_1:4; :: thesis: verum

end;

suppose C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2

then C meets A1 \/ A2 by XBOOLE_0:def 7;
then X0 meets X1 union X2 by A6, TSEP_1:def 3;
then ( the carrier of (X0 meet (X1 union X2)) = C /\ (A1 \/ A2) & the carrier of (X1 meet X2) = A1 /\ A2 ) by A1, A6, TSEP_1:def 5;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A5, TSEP_1:4;
then ( A1 \/ A2 c= A2 \/ (A1 /\ A2) & A1 /\ A2 c= A2 ) by A9, A12, XBOOLE_1:13, XBOOLE_1:17;
hence A1 \/ A2 c= A2 by XBOOLE_1:12; :: thesis: verum

end;

end;

end;

hence A1 \/ A2 c= A2 ; :: thesis: verum

end;

now

assume C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2
then C meets A1 \/ A2 by XBOOLE_0:def 7;
then X0 meets X1 union X2 by A6, TSEP_1:def 3;
then ( the carrier of (X0 meet (X1 union X2)) = C /\ (A1 \/ A2) & the carrier of (X1 meet X2) = A1 /\ A2 ) by A1, A6, TSEP_1:def 5;
then A13: ( C /\ (A1 \/ A2) c= A1 /\ A2 & A1 /\ A2 c= A2 ) by A5, TSEP_1:4, XBOOLE_1:17;
then A14: C /\ (A1 \/ A2) c= A2 by XBOOLE_1:1;

now

per cases ( C2 /\ (A1 \/ A2) = {} or C2 /\ (A1 \/ A2) <> {} ) ;

suppose C2 /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A2

hence A1 \/ A2 c= A2 by A9, A13, XBOOLE_1:1; :: thesis: verum

end;

suppose C2 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2

then C2 meets A1 \/ A2 by XBOOLE_0:def 7;
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 5;
then C2 /\ (A1 \/ A2) c= A2 by A4, TSEP_1:4;
hence A1 \/ A2 c= A2 by A9, A14, XBOOLE_1:8; :: thesis: verum

end;

end;

end;

hence A1 \/ A2 c= A2 ; :: thesis: verum

end;

then ( A1 \/ A2 c= A2 & A1 c= A1 \/ A2 ) by A9, A10, XBOOLE_1:7;
then A1 c= A2 by XBOOLE_1:1;
hence contradiction by A2, TSEP_1:4; :: thesis: verum

end;

now

assume Y2 misses X1 union X2 ; :: thesis: contradiction
then A15: C2 misses A1 \/ A2 by A6, TSEP_1:def 3;
the carrier of X = (C1 \/ C2) \/ C by A3, A6, TSEP_1:def 2;
then A16: A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A15, XBOOLE_0:def 7
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23 ;

A17: now

assume C1 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1
then C1 meets A1 \/ A2 by XBOOLE_0:def 7;
then Y1 meets X1 union X2 by A6, TSEP_1:def 3;
then A18: the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A6, TSEP_1:def 5;
then A19: C1 /\ (A1 \/ A2) c= A1 by A4, TSEP_1:4;

now

per cases ( C /\ (A1 \/ A2) = {} or C /\ (A1 \/ A2) <> {} ) ;

suppose C /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A1

hence A1 \/ A2 c= A1 by A4, A16, A18, TSEP_1:4; :: thesis: verum

end;

suppose C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1

then C meets A1 \/ A2 by XBOOLE_0:def 7;
then X0 meets X1 union X2 by A6, TSEP_1:def 3;
then ( the carrier of (X0 meet (X1 union X2)) = C /\ (A1 \/ A2) & the carrier of (X1 meet X2) = A1 /\ A2 ) by A1, A6, TSEP_1:def 5;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A5, TSEP_1:4;
then ( A1 \/ A2 c= A1 \/ (A1 /\ A2) & A1 /\ A2 c= A1 ) by A16, A19, XBOOLE_1:13, XBOOLE_1:17;
hence A1 \/ A2 c= A1 by XBOOLE_1:12; :: thesis: verum

end;

end;

end;

hence A1 \/ A2 c= A1 ; :: thesis: verum

end;

now

assume C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1
then C meets A1 \/ A2 by XBOOLE_0:def 7;
then X0 meets X1 union X2 by A6, TSEP_1:def 3;
then ( the carrier of (X0 meet (X1 union X2)) = C /\ (A1 \/ A2) & the carrier of (X1 meet X2) = A1 /\ A2 ) by A1, A6, TSEP_1:def 5;
then A20: ( C /\ (A1 \/ A2) c= A1 /\ A2 & A1 /\ A2 c= A1 ) by A5, TSEP_1:4, XBOOLE_1:17;
then A21: C /\ (A1 \/ A2) c= A1 by XBOOLE_1:1;

now

per cases ( C1 /\ (A1 \/ A2) = {} or C1 /\ (A1 \/ A2) <> {} ) ;

suppose C1 /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A1

hence A1 \/ A2 c= A1 by A16, A20, XBOOLE_1:1; :: thesis: verum

end;

suppose C1 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1

then C1 meets A1 \/ A2 by XBOOLE_0:def 7;
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 5;
then C1 /\ (A1 \/ A2) c= A1 by A4, TSEP_1:4;
hence A1 \/ A2 c= A1 by A16, A21, XBOOLE_1:8; :: thesis: verum

end;

end;

end;

hence A1 \/ A2 c= A1 ; :: thesis: verum

end;

then ( A1 \/ A2 c= A1 & A2 c= A1 \/ A2 ) by A16, A17, XBOOLE_1:7;
then A2 c= A1 by XBOOLE_1:1;
hence contradiction by A2, TSEP_1:4; :: thesis: verum

end;

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