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 & 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 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 & 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 ) )
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;
assume that
A2: X1 is not SubSpace of X2 and
A3: 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 A4: 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 that
A5: Y1 meet (X1 union X2) is SubSpace of X1 and
A6: 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 A7: X0 meet (X1 union X2) is SubSpace of X1 meet X2 ; :: thesis: ( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
A8: the carrier of (X1 union X2) = A1 \/ A2 by TSEP_1:def 2;
A9: the carrier of (Y1 union Y2) = C1 \/ C2 by TSEP_1:def 2;
A10: now :: thesis: not Y2 misses X1 union X2
assume Y2 misses X1 union X2 ; :: thesis: contradiction
then A11: C2 misses A1 \/ A2 by A8, TSEP_1:def 3;
the carrier of X = (C1 \/ C2) \/ C by A4, A9, TSEP_1:def 2;
then A12: 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 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23, A11 ;
A13: now :: thesis: ( C1 /\ (A1 \/ A2) <> {} implies A1 \/ A2 c= A1 )
assume C1 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1
then C1 meets A1 \/ A2 ;
then Y1 meets X1 union X2 by A8, TSEP_1:def 3;
then A14: the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A8, TSEP_1:def 4;
then A15: C1 /\ (A1 \/ A2) c= A1 by A5, TSEP_1:4;
now :: thesis: A1 \/ A2 c= A1
per cases ( C /\ (A1 \/ A2) = {} or C /\ (A1 \/ A2) <> {} ) ;
suppose C /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A1
hence A1 \/ A2 c= A1 by A5, A12, A14, TSEP_1:4; :: thesis: verum
end;
suppose C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1
then C meets A1 \/ A2 ;
then X0 meets X1 union X2 by A8, TSEP_1:def 3;
then A16: the carrier of (X0 meet (X1 union X2)) = C /\ (A1 \/ A2) by A8, TSEP_1:def 4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, TSEP_1:def 4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A7, A16, TSEP_1:4;
then A1 \/ A2 c= A1 \/ (A1 /\ A2) by A12, A15, XBOOLE_1:13;
hence A1 \/ A2 c= A1 by XBOOLE_1:12, XBOOLE_1:17; :: thesis: verum
end;
end;
end;
hence A1 \/ A2 c= A1 ; :: thesis: verum
end;
A17: now :: thesis: ( C /\ (A1 \/ A2) <> {} implies A1 \/ A2 c= A1 )
assume C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1
then C meets A1 \/ A2 ;
then X0 meets X1 union X2 by A8, TSEP_1:def 3;
then A18: the carrier of (X0 meet (X1 union X2)) = C /\ (A1 \/ A2) by A8, TSEP_1:def 4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, TSEP_1:def 4;
then A19: C /\ (A1 \/ A2) c= A1 /\ A2 by A7, A18, TSEP_1:4;
A20: A1 /\ A2 c= A1 by XBOOLE_1:17;
then A21: C /\ (A1 \/ A2) c= A1 by A19, XBOOLE_1:1;
now :: thesis: A1 \/ A2 c= A1
per cases ( C1 /\ (A1 \/ A2) = {} or C1 /\ (A1 \/ A2) <> {} ) ;
suppose C1 /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A1
hence A1 \/ A2 c= A1 by A12, A19, A20, XBOOLE_1:1; :: thesis: verum
end;
suppose C1 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1
then C1 meets A1 \/ A2 ;
then Y1 meets X1 union X2 by A8, TSEP_1:def 3;
then the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A8, TSEP_1:def 4;
then C1 /\ (A1 \/ A2) c= A1 by A5, TSEP_1:4;
hence A1 \/ A2 c= A1 by A12, A21, XBOOLE_1:8; :: thesis: verum
end;
end;
end;
hence A1 \/ A2 c= A1 ; :: thesis: verum
end;
A2 c= A1 \/ A2 by XBOOLE_1:7;
then A2 c= A1 by A12, A13, A17, XBOOLE_1:1;
hence contradiction by A3, TSEP_1:4; :: thesis: verum
end;
now :: thesis: not Y1 misses X1 union X2
assume Y1 misses X1 union X2 ; :: thesis: contradiction
then A22: C1 misses A1 \/ A2 by A8, TSEP_1:def 3;
the carrier of X = (C1 \/ C2) \/ C by A4, A9, TSEP_1:def 2;
then A23: 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 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23, A22 ;
A24: now :: thesis: ( C2 /\ (A1 \/ A2) <> {} implies A1 \/ A2 c= A2 )
assume C2 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2
then C2 meets A1 \/ A2 ;
then Y2 meets X1 union X2 by A8, TSEP_1:def 3;
then A25: the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A8, TSEP_1:def 4;
then A26: C2 /\ (A1 \/ A2) c= A2 by A6, TSEP_1:4;
now :: thesis: A1 \/ A2 c= A2
per cases ( C /\ (A1 \/ A2) = {} or C /\ (A1 \/ A2) <> {} ) ;
suppose C /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A2
hence A1 \/ A2 c= A2 by A6, A23, A25, TSEP_1:4; :: thesis: verum
end;
suppose C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2
then C meets A1 \/ A2 ;
then X0 meets X1 union X2 by A8, TSEP_1:def 3;
then A27: the carrier of (X0 meet (X1 union X2)) = C /\ (A1 \/ A2) by A8, TSEP_1:def 4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, TSEP_1:def 4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A7, A27, TSEP_1:4;
then A1 \/ A2 c= A2 \/ (A1 /\ A2) by A23, A26, XBOOLE_1:13;
hence A1 \/ A2 c= A2 by XBOOLE_1:12, XBOOLE_1:17; :: thesis: verum
end;
end;
end;
hence A1 \/ A2 c= A2 ; :: thesis: verum
end;
A28: now :: thesis: ( C /\ (A1 \/ A2) <> {} implies A1 \/ A2 c= A2 )
assume C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2
then C meets A1 \/ A2 ;
then X0 meets X1 union X2 by A8, TSEP_1:def 3;
then A29: the carrier of (X0 meet (X1 union X2)) = C /\ (A1 \/ A2) by A8, TSEP_1:def 4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, TSEP_1:def 4;
then A30: C /\ (A1 \/ A2) c= A1 /\ A2 by A7, A29, TSEP_1:4;
A31: A1 /\ A2 c= A2 by XBOOLE_1:17;
then A32: C /\ (A1 \/ A2) c= A2 by A30, XBOOLE_1:1;
now :: thesis: A1 \/ A2 c= A2
per cases ( C2 /\ (A1 \/ A2) = {} or C2 /\ (A1 \/ A2) <> {} ) ;
suppose C2 /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A2
hence A1 \/ A2 c= A2 by A23, A30, A31, XBOOLE_1:1; :: thesis: verum
end;
suppose C2 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2
then C2 meets A1 \/ A2 ;
then Y2 meets X1 union X2 by A8, TSEP_1:def 3;
then the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A8, TSEP_1:def 4;
then C2 /\ (A1 \/ A2) c= A2 by A6, TSEP_1:4;
hence A1 \/ A2 c= A2 by A23, A32, XBOOLE_1:8; :: thesis: verum
end;
end;
end;
hence A1 \/ A2 c= A2 ; :: thesis: verum
end;
A1 c= A1 \/ A2 by XBOOLE_1:7;
then A1 c= A2 by A23, A24, A28, 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 A10; :: thesis: verum