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;

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

then A2 c= A1 by A12, A13, A17, XBOOLE_1:1;

hence contradiction by A3, TSEP_1:4; :: thesis: verum

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

end;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= A1end;

hence
A1 \/ A2 c= A1
; :: thesis: verumper cases
( C /\ (A1 \/ A2) = {} or C /\ (A1 \/ A2) <> {} )
;

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

A17: now :: thesis: ( C /\ (A1 \/ A2) <> {} implies A1 \/ A2 c= A1 )

A2 c= A1 \/ A2
by XBOOLE_1:7;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;

end;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= A1end;

hence
A1 \/ A2 c= A1
; :: thesis: verumper cases
( C1 /\ (A1 \/ A2) = {} or C1 /\ (A1 \/ A2) <> {} )
;

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

then A2 c= A1 by A12, A13, A17, XBOOLE_1:1;

hence contradiction by A3, TSEP_1:4; :: thesis: verum

now :: thesis: not Y1 misses X1 union X2

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

then A1 c= A2 by A23, A24, A28, XBOOLE_1:1;

hence contradiction by A2, TSEP_1:4; :: thesis: verum

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

end;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= A2end;

hence
A1 \/ A2 c= A2
; :: thesis: verumper cases
( C /\ (A1 \/ A2) = {} or C /\ (A1 \/ A2) <> {} )
;

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

A28: now :: thesis: ( C /\ (A1 \/ A2) <> {} implies A1 \/ A2 c= A2 )

A1 c= A1 \/ A2
by XBOOLE_1:7;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;

end;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= A2end;

hence
A1 \/ A2 c= A2
; :: thesis: verumper cases
( C2 /\ (A1 \/ A2) = {} or C2 /\ (A1 \/ A2) <> {} )
;

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

then A1 c= A2 by A23, A24, A28, XBOOLE_1:1;

hence contradiction by A2, TSEP_1:4; :: thesis: verum