let X be set ; :: thesis: ( X <> {} implies ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in Y holds
Y1 misses X ) ) )
defpred S1[ set ] means ex Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 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, Y5 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in $1 & Y1 meets X );
defpred S7[ 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 );
defpred S8[ set ] means 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 $1 & Y1 meets X );
defpred S9[ set ] means ex Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8 being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 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) & S9[Y] ) ) from XBOOLE_0:sch 1();
 consider Z5 being set such that
A3: for Y being set holds
( Y in Z5 iff ( Y in union (union (union (union (union X)))) & S6[Y] ) ) from XBOOLE_0:sch 1();
 defpred S10[ 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 );
consider Z6 being set such that
A4: for Y being set holds
( Y in Z6 iff ( Y in union (union (union (union (union (union X))))) & S10[Y] ) ) from XBOOLE_0:sch 1();
 consider ZA being set such that
A5: for Y being set holds
( Y in ZA iff ( Y in union (union (union (union (union (union (union (union (union (union X))))))))) & S2[Y] ) ) from XBOOLE_0:sch 1();
 consider Z3 being set such that
A6: for Y being set holds
( Y in Z3 iff ( Y in union (union (union X)) & S8[Y] ) ) from XBOOLE_0:sch 1();
 consider Z7 being set such that
A7: for Y being set holds
( Y in Z7 iff ( Y in union (union (union (union (union (union (union X)))))) & S5[Y] ) ) from XBOOLE_0:sch 1();
 consider Z4 being set such that
A8: for Y being set holds
( Y in Z4 iff ( Y in union (union (union (union X))) & S7[Y] ) ) from XBOOLE_0:sch 1();
 consider Z9 being set such that
A9: for Y being set holds
( Y in Z9 iff ( Y in union (union (union (union (union (union (union (union (union X)))))))) & S3[Y] ) ) from XBOOLE_0:sch 1();
 consider Z8 being set such that
A10: for Y being set holds
( Y in Z8 iff ( Y in union (union (union (union (union (union (union (union X))))))) & S4[Y] ) ) from XBOOLE_0:sch 1();
 set V = (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA;
assume X <> {} ; :: thesis: ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in Y holds
Y1 misses X ) )
then consider Y being set such that
A11: Y in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA and
A12: Y misses (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by MCART_1:1;
A13: (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA = ((((((((X \/ (Z1 \/ Z2)) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4
.= (((((((X \/ ((Z1 \/ Z2) \/ Z3)) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4
.= ((((((X \/ (((Z1 \/ Z2) \/ Z3) \/ Z4)) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4
.= (((((X \/ ((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5)) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4
.= ((((X \/ (((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6)) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4
.= (((X \/ ((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7)) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4
.= ((X \/ (((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8)) \/ Z9) \/ ZA by XBOOLE_1:4
.= (X \/ ((((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9)) \/ ZA by XBOOLE_1:4
.= X \/ (((((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) by XBOOLE_1:4 ;
A14: now
assume A15: Y in Z1 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set such that
A16: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 ) and
A17: Y9 in Y and
A18: Y1 meets X by A1;
Y in union X by A1, A15;
then Y9 in union (union X) by A17, TARSKI:def 4;
then Y9 in Z2 by A2, A16, A18;
then Y9 in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
then Y meets (X \/ Z1) \/ Z2 by A17, 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;
then Y meets ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_1:70;
then Y meets (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_1:70;
then Y meets ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_1:70;
hence contradiction by A12, XBOOLE_1:70; :: thesis: verum
end;
assume A19: for Y being set holds
( not Y in X or ex Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA being set st
( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA & YA in Y & not Y1 misses X ) ) ; :: thesis: contradiction
now
assume A20: Y in X ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA being set such that
A21: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y9 & Y9 in YA ) and
A22: YA in Y and
A23: not Y1 misses X by A19;
YA in union X by A20, A22, TARSKI:def 4;
then YA in Z1 by A1, A21, A23;
then YA in X \/ Z1 by XBOOLE_0:def 3;
then YA in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
then YA in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def 3;
then YA in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
then YA in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
then Y meets ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by A22, XBOOLE_0:3;
then Y meets (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_1:70;
then Y meets ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_1:70;
then Y meets (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_1:70;
then Y meets ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_1:70;
hence contradiction by A12, XBOOLE_1:70; :: thesis: verum
end;
then Y in ((((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by A13, A11, XBOOLE_0:def 3;
then Y in (((((((Z1 \/ (Z2 \/ Z3)) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in ((((((Z1 \/ ((Z2 \/ Z3) \/ Z4)) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (((((Z1 \/ (((Z2 \/ Z3) \/ Z4) \/ Z5)) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in ((((Z1 \/ ((((Z2 \/ Z3) \/ Z4) \/ Z5) \/ Z6)) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (((Z1 \/ (((((Z2 \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7)) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in ((Z1 \/ ((((((Z2 \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8)) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (Z1 \/ (((((((Z2 \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9)) \/ ZA by XBOOLE_1:4;
then Y in Z1 \/ ((((((((Z2 \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) by XBOOLE_1:4;
then Y in (((((((Z2 \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by A14, XBOOLE_0:def 3;
then Y in ((((((Z2 \/ (Z3 \/ Z4)) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (((((Z2 \/ ((Z3 \/ Z4) \/ Z5)) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in ((((Z2 \/ (((Z3 \/ Z4) \/ Z5) \/ Z6)) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (((Z2 \/ ((((Z3 \/ Z4) \/ Z5) \/ Z6) \/ Z7)) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in ((Z2 \/ (((((Z3 \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8)) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (Z2 \/ ((((((Z3 \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9)) \/ ZA by XBOOLE_1:4;
then A24: Y in Z2 \/ (((((((Z3 \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) by XBOOLE_1:4;
A25: now
assume A26: Y in Z3 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set such that
A27: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 ) and
A28: Y7 in Y and
A29: Y1 meets X by A6;
Y in union (union (union X)) by A6, A26;
then Y7 in union (union (union (union X))) by A28, TARSKI:def 4;
then Y7 in Z4 by A8, A27, A29;
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 Y7 in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_0:def 3;
then Y7 in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
then Y7 in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_0:def 3;
then Y7 in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then Y7 in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
hence contradiction by A12, A28, XBOOLE_0:3; :: thesis: verum
end;
A30: now
assume A31: Y in Z4 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6 being set such that
A32: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 ) and
A33: Y6 in Y and
A34: Y1 meets X by A8;
Y in union (union (union (union X))) by A8, A31;
then Y6 in union (union (union (union (union X)))) by A33, TARSKI:def 4;
then Y6 in Z5 by A3, A32, A34;
then Y6 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
then Y6 in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_0:def 3;
then Y6 in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
then Y6 in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_0:def 3;
then Y6 in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then Y6 in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
hence contradiction by A12, A33, XBOOLE_0:3; :: thesis: verum
end;
A35: now
assume A36: Y in Z5 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5 being set such that
A37: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 ) and
A38: Y5 in Y and
A39: Y1 meets X by A3;
Y in union (union (union (union (union X)))) by A3, A36;
then Y5 in union (union (union (union (union (union X))))) by A38, TARSKI:def 4;
then Y5 in Z6 by A4, A37, A39;
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;
then Y5 in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_0:def 3;
then Y5 in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then Y5 in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
hence contradiction by A12, A38, XBOOLE_0:3; :: thesis: verum
end;
now
assume A40: Y in Z2 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8 being set such that
A41: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 ) and
A42: Y8 in Y and
A43: Y1 meets X by A2;
Y in union (union X) by A2, A40;
then Y8 in union (union (union X)) by A42, TARSKI:def 4;
then Y8 in Z3 by A6, A41, A43;
then Y8 in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def 3;
then Y8 in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
then Y8 in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
then Y8 in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_0:def 3;
then Y8 in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
then Y8 in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_0:def 3;
then Y8 in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then Y8 in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
hence contradiction by A12, A42, XBOOLE_0:3; :: thesis: verum
end;
then Y in ((((((Z3 \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by A24, XBOOLE_0:def 3;
then Y in (((((Z3 \/ (Z4 \/ Z5)) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in ((((Z3 \/ ((Z4 \/ Z5) \/ Z6)) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (((Z3 \/ (((Z4 \/ Z5) \/ Z6) \/ Z7)) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in ((Z3 \/ ((((Z4 \/ Z5) \/ Z6) \/ Z7) \/ Z8)) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (Z3 \/ (((((Z4 \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9)) \/ ZA by XBOOLE_1:4;
then Y in Z3 \/ ((((((Z4 \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) by XBOOLE_1:4;
then Y in (((((Z4 \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by A25, XBOOLE_0:def 3;
then Y in ((((Z4 \/ (Z5 \/ Z6)) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (((Z4 \/ ((Z5 \/ Z6) \/ Z7)) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in ((Z4 \/ (((Z5 \/ Z6) \/ Z7) \/ Z8)) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (Z4 \/ ((((Z5 \/ Z6) \/ Z7) \/ Z8) \/ Z9)) \/ ZA by XBOOLE_1:4;
then Y in Z4 \/ (((((Z5 \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) by XBOOLE_1:4;
then Y in ((((Z5 \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by A30, XBOOLE_0:def 3;
then Y in (((Z5 \/ (Z6 \/ Z7)) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in ((Z5 \/ ((Z6 \/ Z7) \/ Z8)) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (Z5 \/ (((Z6 \/ Z7) \/ Z8) \/ Z9)) \/ ZA by XBOOLE_1:4;
then Y in Z5 \/ ((((Z6 \/ Z7) \/ Z8) \/ Z9) \/ ZA) by XBOOLE_1:4;
then Y in (((Z6 \/ Z7) \/ Z8) \/ Z9) \/ ZA by A35, XBOOLE_0:def 3;
then Y in ((Z6 \/ (Z7 \/ Z8)) \/ Z9) \/ ZA by XBOOLE_1:4;
then Y in (Z6 \/ ((Z7 \/ Z8) \/ Z9)) \/ ZA by XBOOLE_1:4;
then A44: Y in Z6 \/ (((Z7 \/ Z8) \/ Z9) \/ ZA) by XBOOLE_1:4;
A45: now
assume A46: Y in Z7 ; :: thesis: contradiction
then consider Y1, Y2, Y3 being set such that
A47: ( Y1 in Y2 & Y2 in Y3 ) and
A48: Y3 in Y and
A49: Y1 meets X by A7;
Y in union (union (union (union (union (union (union X)))))) by A7, A46;
then Y3 in union (union (union (union (union (union (union (union X))))))) by A48, TARSKI:def 4;
then Y3 in Z8 by A10, A47, A49;
then Y3 in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_0:def 3;
then Y3 in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then Y3 in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
hence contradiction by A12, A48, XBOOLE_0:3; :: thesis: verum
end;
A50: now
assume A51: Y in Z8 ; :: thesis: contradiction
then consider Y1, Y2 being set such that
A52: Y1 in Y2 and
A53: Y2 in Y and
A54: Y1 meets X by A10;
Y in union (union (union (union (union (union (union (union X))))))) by A10, A51;
then Y2 in union (union (union (union (union (union (union (union (union X)))))))) by A53, TARSKI:def 4;
then Y2 in Z9 by A9, A52, A54;
then Y2 in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then Y2 in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
hence contradiction by A12, A53, XBOOLE_0:3; :: thesis: verum
end;
A55: now
assume A56: Y in Z9 ; :: thesis: contradiction
then consider Y1 being set such that
A57: Y1 in Y and
A58: Y1 meets X by A9;
Y in union (union (union (union (union (union (union (union (union X)))))))) by A9, A56;
then Y1 in union (union (union (union (union (union (union (union (union (union X))))))))) by A57, TARSKI:def 4;
then Y1 in ZA by A5, A58;
then Y1 in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
hence contradiction by A12, A57, XBOOLE_0:3; :: thesis: verum
end;
now
assume A59: Y in Z6 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4 being set such that
A60: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 ) and
A61: Y4 in Y and
A62: Y1 meets X by A4;
Y in union (union (union (union (union (union X))))) by A4, A59;
then Y4 in union (union (union (union (union (union (union X)))))) by A61, TARSKI:def 4;
then Y4 in Z7 by A7, A60, A62;
then Y4 in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
then Y4 in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_0:def 3;
then Y4 in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then Y4 in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
hence contradiction by A12, A61, XBOOLE_0:3; :: thesis: verum
end;
then Y in ((Z7 \/ Z8) \/ Z9) \/ ZA by A44, XBOOLE_0:def 3;
then Y in (Z7 \/ (Z8 \/ Z9)) \/ ZA by XBOOLE_1:4;
then Y in Z7 \/ ((Z8 \/ Z9) \/ ZA) by XBOOLE_1:4;
then Y in (Z8 \/ Z9) \/ ZA by A45, XBOOLE_0:def 3;
then Y in Z8 \/ (Z9 \/ ZA) by XBOOLE_1:4;
then Y in Z9 \/ ZA by A50, XBOOLE_0:def 3;
then Y in ZA by A55, XBOOLE_0:def 3;
then Y meets X by A5;
hence contradiction by A13, A12, XBOOLE_1:70; :: thesis: verum