let X be set ; :: thesis: ( X <> {} implies ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y holds
Y1 misses X ) ) )
defpred S1[ set ] means ex Y1, Y2, Y3, Y4, Y5, Y6 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in $1 & Y1 meets X );
consider Z1 being set such that
A1: for Y being set holds
( Y in Z1 iff ( Y in union X & S1[Y] ) ) from XBOOLE_0:sch 1();
 defpred S2[ set ] means $1 meets X;
defpred S3[ set ] means ex Y1 being set st
( Y1 in $1 & Y1 meets X );
defpred S4[ set ] means ex Y1, Y2 being set st
( Y1 in Y2 & Y2 in $1 & Y1 meets X );
defpred S5[ set ] means ex Y1, Y2, Y3 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X );
defpred S6[ set ] means ex Y1, Y2, Y3, Y4 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in $1 & Y1 meets X );
defpred S7[ set ] means ex Y1, Y2, Y3, Y4, Y5 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in $1 & Y1 meets X );
consider Z2 being set such that
A2: for Y being set holds
( Y in Z2 iff ( Y in union (union X) & S7[Y] ) ) from XBOOLE_0:sch 1();
 consider Z7 being set such that
A3: for Y being set holds
( Y in Z7 iff ( Y in union (union (union (union (union (union (union X)))))) & S2[Y] ) ) from XBOOLE_0:sch 1();
 consider Z3 being set such that
A4: for Y being set holds
( Y in Z3 iff ( Y in union (union (union X)) & S6[Y] ) ) from XBOOLE_0:sch 1();
 consider Z6 being set such that
A5: for Y being set holds
( Y in Z6 iff ( Y in union (union (union (union (union (union X))))) & S3[Y] ) ) from XBOOLE_0:sch 1();
 consider Z5 being set such that
A6: for Y being set holds
( Y in Z5 iff ( Y in union (union (union (union (union X)))) & S4[Y] ) ) from XBOOLE_0:sch 1();
 consider Z4 being set such that
A7: for Y being set holds
( Y in Z4 iff ( Y in union (union (union (union X))) & S5[Y] ) ) from XBOOLE_0:sch 1();
 set V = ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7;
assume X <> {} ; :: thesis: ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y holds
Y1 misses X ) )
then consider Y being set such that
A8: Y in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 and
A9: Y misses ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by MCART_1:1;
A10: ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 = (((((X \/ (Z1 \/ Z2)) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_1:4
.= ((((X \/ ((Z1 \/ Z2) \/ Z3)) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_1:4
.= (((X \/ (((Z1 \/ Z2) \/ Z3) \/ Z4)) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_1:4
.= ((X \/ ((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5)) \/ Z6) \/ Z7 by XBOOLE_1:4
.= (X \/ (((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6)) \/ Z7 by XBOOLE_1:4
.= X \/ ((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) by XBOOLE_1:4 ;
A11: now
assume A12: Y in Z1 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6 being set such that
A13: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 ) and
A14: Y6 in Y and
A15: Y1 meets X by A1;
Y in union X by A1, A12;
then Y6 in union (union X) by A14, TARSKI:def 4;
then Y6 in Z2 by A2, A13, A15;
then Y6 in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
then Y meets (X \/ Z1) \/ Z2 by A14, XBOOLE_0:3;
then Y meets ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_1:70;
then Y meets (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_1:70;
then Y meets ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_1:70;
then Y meets (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_1:70;
hence contradiction by A9, XBOOLE_1:70; :: thesis: verum
end;
A16: now
assume A17: Y in Z2 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5 being set such that
A18: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 ) and
A19: Y5 in Y and
A20: Y1 meets X by A2;
Y in union (union X) by A2, A17;
then Y5 in union (union (union X)) by A19, TARSKI:def 4;
then Y5 in Z3 by A4, A18, A20;
then Y5 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def 3;
then Y5 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
then Y5 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
then Y5 in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_0:def 3;
then Y5 in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
hence contradiction by A9, A19, XBOOLE_0:3; :: thesis: verum
end;
assume A21: for Y being set holds
( not Y in X or ex Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y & not Y1 misses X ) ) ; :: thesis: contradiction
now
assume A22: Y in X ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set such that
A23: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 ) and
A24: Y7 in Y and
A25: not Y1 misses X by A21;
Y7 in union X by A22, A24, TARSKI:def 4;
then Y7 in Z1 by A1, A23, A25;
then Y7 in X \/ Z1 by XBOOLE_0:def 3;
then Y7 in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
then Y7 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def 3;
then Y7 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
then Y7 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
then Y meets ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by A24, XBOOLE_0:3;
then Y meets (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_1:70;
hence contradiction by A9, XBOOLE_1:70; :: thesis: verum
end;
then Y in (((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by A10, A8, XBOOLE_0:def 3;
then Y in ((((Z1 \/ (Z2 \/ Z3)) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_1:4;
then Y in (((Z1 \/ ((Z2 \/ Z3) \/ Z4)) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_1:4;
then Y in ((Z1 \/ (((Z2 \/ Z3) \/ Z4) \/ Z5)) \/ Z6) \/ Z7 by XBOOLE_1:4;
then Y in (Z1 \/ ((((Z2 \/ Z3) \/ Z4) \/ Z5) \/ Z6)) \/ Z7 by XBOOLE_1:4;
then Y in Z1 \/ (((((Z2 \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) by XBOOLE_1:4;
then Y in ((((Z2 \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by A11, XBOOLE_0:def 3;
then Y in (((Z2 \/ (Z3 \/ Z4)) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_1:4;
then Y in ((Z2 \/ ((Z3 \/ Z4) \/ Z5)) \/ Z6) \/ Z7 by XBOOLE_1:4;
then Y in (Z2 \/ (((Z3 \/ Z4) \/ Z5) \/ Z6)) \/ Z7 by XBOOLE_1:4;
then Y in Z2 \/ ((((Z3 \/ Z4) \/ Z5) \/ Z6) \/ Z7) by XBOOLE_1:4;
then Y in (((Z3 \/ Z4) \/ Z5) \/ Z6) \/ Z7 by A16, XBOOLE_0:def 3;
then Y in ((Z3 \/ (Z4 \/ Z5)) \/ Z6) \/ Z7 by XBOOLE_1:4;
then Y in (Z3 \/ ((Z4 \/ Z5) \/ Z6)) \/ Z7 by XBOOLE_1:4;
then A26: Y in Z3 \/ (((Z4 \/ Z5) \/ Z6) \/ Z7) by XBOOLE_1:4;
A27: now
assume A28: Y in Z4 ; :: thesis: contradiction
then consider Y1, Y2, Y3 being set such that
A29: ( Y1 in Y2 & Y2 in Y3 ) and
A30: Y3 in Y and
A31: Y1 meets X by A7;
Y in union (union (union (union X))) by A7, A28;
then Y3 in union (union (union (union (union X)))) by A30, TARSKI:def 4;
then Y3 in Z5 by A6, A29, A31;
then Y3 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
then Y3 in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_0:def 3;
then Y3 in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
hence contradiction by A9, A30, XBOOLE_0:3; :: thesis: verum
end;
A32: now
assume A33: Y in Z5 ; :: thesis: contradiction
then consider Y1, Y2 being set such that
A34: Y1 in Y2 and
A35: Y2 in Y and
A36: Y1 meets X by A6;
Y in union (union (union (union (union X)))) by A6, A33;
then Y2 in union (union (union (union (union (union X))))) by A35, TARSKI:def 4;
then Y2 in Z6 by A5, A34, A36;
then Y2 in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_0:def 3;
then Y2 in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
hence contradiction by A9, A35, XBOOLE_0:3; :: thesis: verum
end;
A37: now
assume A38: Y in Z6 ; :: thesis: contradiction
then consider Y1 being set such that
A39: Y1 in Y and
A40: Y1 meets X by A5;
Y in union (union (union (union (union (union X))))) by A5, A38;
then Y1 in union (union (union (union (union (union (union X)))))) by A39, TARSKI:def 4;
then Y1 in Z7 by A3, A40;
then Y1 in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
hence contradiction by A9, A39, XBOOLE_0:3; :: thesis: verum
end;
now
assume A41: Y in Z3 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4 being set such that
A42: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 ) and
A43: Y4 in Y and
A44: Y1 meets X by A4;
Y in union (union (union X)) by A4, A41;
then Y4 in union (union (union (union X))) by A43, TARSKI:def 4;
then Y4 in Z4 by A7, A42, A44;
then Y4 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
then Y4 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
then Y4 in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_0:def 3;
then Y4 in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
hence contradiction by A9, A43, XBOOLE_0:3; :: thesis: verum
end;
then Y in ((Z4 \/ Z5) \/ Z6) \/ Z7 by A26, XBOOLE_0:def 3;
then Y in (Z4 \/ (Z5 \/ Z6)) \/ Z7 by XBOOLE_1:4;
then Y in Z4 \/ ((Z5 \/ Z6) \/ Z7) by XBOOLE_1:4;
then Y in (Z5 \/ Z6) \/ Z7 by A27, XBOOLE_0:def 3;
then Y in Z5 \/ (Z6 \/ Z7) by XBOOLE_1:4;
then Y in Z6 \/ Z7 by A32, XBOOLE_0:def 3;
then Y in Z7 by A37, XBOOLE_0:def 3;
then Y meets X by A3;
hence contradiction by A10, A9, XBOOLE_1:70; :: thesis: verum