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, YB, YC, YD, YE, YF 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 YB & YB in YC & YC in YD & YD in YE & YE in YF & YF in Y holds
Y1 misses X ) ) )
defpred S1[ set ] means ex Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD, YE 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 YB & YB in YC & YC in YD & YD in YE & YE 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 );
defpred S8[ 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 S9[ 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 S10[ 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 );
defpred S11[ 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 );
defpred S12[ set ] means 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 $1 & Y1 meets X );
defpred S13[ set ] means ex Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB 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 YB & YB in $1 & Y1 meets X );
defpred S14[ set ] means ex Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC 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 YB & YB in YC & YC in $1 & Y1 meets X );
defpred S15[ set ] means ex Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD 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 YB & YB in YC & YC in YD & YD 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) & S15[Y] ) ) from XBOOLE_0:sch 1();
 consider Z9 being set such that
A3: for Y being set holds
( Y in Z9 iff ( Y in union (union (union (union (union (union (union (union (union X)))))))) & S8[Y] ) ) from XBOOLE_0:sch 1();
 consider Z8 being set such that
A4: for Y being set holds
( Y in Z8 iff ( Y in union (union (union (union (union (union (union (union X))))))) & S9[Y] ) ) from XBOOLE_0:sch 1();
 consider ZF being set such that
A5: for Y being set holds
( Y in ZF iff ( Y in union (union (union (union (union (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)) & S14[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)))))) & S10[Y] ) ) from XBOOLE_0:sch 1();
 consider Z6 being set such that
A8: for Y being set holds
( Y in Z6 iff ( Y in union (union (union (union (union (union X))))) & S11[Y] ) ) from XBOOLE_0:sch 1();
 consider ZE being set such that
A9: for Y being set holds
( Y in ZE iff ( Y in union (union (union (union (union (union (union (union (union (union (union (union (union (union X))))))))))))) & S3[Y] ) ) from XBOOLE_0:sch 1();
 consider Z5 being set such that
A10: for Y being set holds
( Y in Z5 iff ( Y in union (union (union (union (union X)))) & S12[Y] ) ) from XBOOLE_0:sch 1();
 consider Z4 being set such that
A11: for Y being set holds
( Y in Z4 iff ( Y in union (union (union (union X))) & S13[Y] ) ) from XBOOLE_0:sch 1();
 consider ZD being set such that
A12: for Y being set holds
( Y in ZD iff ( Y in union (union (union (union (union (union (union (union (union (union (union (union (union X)))))))))))) & S4[Y] ) ) from XBOOLE_0:sch 1();
 consider ZC being set such that
A13: for Y being set holds
( Y in ZC iff ( Y in union (union (union (union (union (union (union (union (union (union (union (union X))))))))))) & S5[Y] ) ) from XBOOLE_0:sch 1();
 consider ZB being set such that
A14: for Y being set holds
( Y in ZB iff ( Y in union (union (union (union (union (union (union (union (union (union (union X)))))))))) & S6[Y] ) ) from XBOOLE_0:sch 1();
 consider ZA being set such that
A15: for Y being set holds
( Y in ZA iff ( Y in union (union (union (union (union (union (union (union (union (union X))))))))) & S7[Y] ) ) from XBOOLE_0:sch 1();
 set V = ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF;
A16: ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF = (((((((((((((X \/ (Z1 \/ Z2)) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_1:4
.= ((((((((((((X \/ ((Z1 \/ Z2) \/ Z3)) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_1:4
.= (((((((((((X \/ (((Z1 \/ Z2) \/ Z3) \/ Z4)) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_1:4
.= ((((((((((X \/ ((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5)) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_1:4
.= (((((((((X \/ (((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6)) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_1:4
.= ((((((((X \/ ((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7)) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_1:4
.= (((((((X \/ (((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8)) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_1:4
.= ((((((X \/ ((((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9)) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_1:4
.= (((((X \/ (((((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA)) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_1:4
.= ((((X \/ ((((((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB)) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_1:4
.= (((X \/ (((((((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC)) \/ ZD) \/ ZE) \/ ZF by XBOOLE_1:4
.= ((X \/ ((((((((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD)) \/ ZE) \/ ZF by XBOOLE_1:4
.= (X \/ (((((((((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE)) \/ ZF by XBOOLE_1:4
.= X \/ ((((((((((((((Z1 \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF) by XBOOLE_1:4 ;
assume X <> {} ; :: thesis: ex Y being set st
( Y in X & ( for Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD, YE, YF 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 YB & YB in YC & YC in YD & YD in YE & YE in YF & YF in Y holds
Y1 misses X ) )
then consider Y being set such that
A17: Y in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF and
A18: Y misses ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by MCART_1:1;
( Y in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE or Y in ZF ) by A17, XBOOLE_0:def 3;
then ( Y in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then ( Y in (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then ( Y in ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then ( Y in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then ( Y in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then ( Y in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then ( Y in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then ( Y in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 or Y in Z7 or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then ( Y in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 or Y in Z6 or Y in Z7 or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then ( Y in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 or Y in Z5 or Y in Z6 or Y in Z7 or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then ( Y in ((X \/ Z1) \/ Z2) \/ Z3 or Y in Z4 or Y in Z5 or Y in Z6 or Y in Z7 or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then ( Y in (X \/ Z1) \/ Z2 or Y in Z3 or Y in Z4 or Y in Z5 or Y in Z6 or Y in Z7 or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
then A19: ( Y in X \/ Z1 or Y in Z2 or Y in Z3 or Y in Z4 or Y in Z5 or Y in Z6 or Y in Z7 or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by XBOOLE_0:def 3;
assume A20: for Y being set holds
( not Y in X or ex Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD, YE, YF 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 YB & YB in YC & YC in YD & YD in YE & YE in YF & YF in Y & not Y1 misses X ) ) ; :: thesis: contradiction
per cases ( Y in X or Y in Z1 or Y in Z2 or Y in Z3 or Y in Z4 or Y in Z5 or Y in Z6 or Y in Z7 or Y in Z8 or Y in Z9 or Y in ZA or Y in ZB or Y in ZC or Y in ZD or Y in ZE or Y in ZF ) by A19, XBOOLE_0:def 3;
suppose A21: Y in X ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD, YE, YF being set such that
A22: ( 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 YB & YB in YC & YC in YD & YD in YE & YE in YF ) and
A23: YF in Y and
A24: not Y1 misses X by A20;
YF in union X by A21, A23, TARSKI:def 4;
then YF in Z1 by A1, A22, A24;
then YF in X \/ Z1 by XBOOLE_0:def 3;
then YF in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
then YF in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def 3;
then YF in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
then YF in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
then Y meets ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by A23, 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;
then Y meets (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:70;
then Y meets ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB by XBOOLE_1:70;
then Y meets (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_1:70;
then Y meets ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_1:70;
then Y meets (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_1:70;
hence contradiction by A18, XBOOLE_1:70; :: thesis: verum
end;
suppose A25: Y in Z1 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD, YE being set such that
A26: ( 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 YB & YB in YC & YC in YD & YD in YE ) and
A27: YE in Y and
A28: Y1 meets X by A1;
Y in union X by A1, A25;
then YE in union (union X) by A27, TARSKI:def 4;
then YE in Z2 by A2, A26, A28;
then YE in (X \/ Z1) \/ Z2 by XBOOLE_0:def 3;
then Y meets (X \/ Z1) \/ Z2 by A27, 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;
then Y meets (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_1:70;
then Y meets ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB by XBOOLE_1:70;
then Y meets (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_1:70;
then Y meets ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_1:70;
then Y meets (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_1:70;
hence contradiction by A18, XBOOLE_1:70; :: thesis: verum
end;
suppose A29: Y in Z2 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC, YD being set such that
A30: ( 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 YB & YB in YC & YC in YD ) and
A31: YD in Y and
A32: Y1 meets X by A2;
Y in union (union X) by A2, A29;
then YD in union (union (union X)) by A31, TARSKI:def 4;
then YD in Z3 by A6, A30, A32;
then YD in ((X \/ Z1) \/ Z2) \/ Z3 by XBOOLE_0:def 3;
then YD in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
then YD in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
then YD in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_0:def 3;
then YD in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
then YD in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_0:def 3;
then YD in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then YD in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
then YD in ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB by XBOOLE_0:def 3;
then YD in (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_0:def 3;
then YD in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_0:def 3;
then YD in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then YD in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A31, XBOOLE_0:3; :: thesis: verum
end;
suppose A33: Y in Z3 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB, YC being set such that
A34: ( 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 YB & YB in YC ) and
A35: YC in Y and
A36: Y1 meets X by A6;
Y in union (union (union X)) by A6, A33;
then YC in union (union (union (union X))) by A35, TARSKI:def 4;
then YC in Z4 by A11, A34, A36;
then YC in (((X \/ Z1) \/ Z2) \/ Z3) \/ Z4 by XBOOLE_0:def 3;
then YC in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
then YC in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_0:def 3;
then YC in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
then YC in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_0:def 3;
then YC in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then YC in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
then YC in ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB by XBOOLE_0:def 3;
then YC in (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_0:def 3;
then YC in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_0:def 3;
then YC in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then YC in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A35, XBOOLE_0:3; :: thesis: verum
end;
suppose A37: Y in Z4 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA, YB being set such that
A38: ( 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 YB ) and
A39: YB in Y and
A40: Y1 meets X by A11;
Y in union (union (union (union X))) by A11, A37;
then YB in union (union (union (union (union X)))) by A39, TARSKI:def 4;
then YB in Z5 by A10, A38, A40;
then YB in ((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5 by XBOOLE_0:def 3;
then YB in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_0:def 3;
then YB in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
then YB in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_0:def 3;
then YB in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then YB in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
then YB in ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB by XBOOLE_0:def 3;
then YB in (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_0:def 3;
then YB in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_0:def 3;
then YB in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then YB in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A39, XBOOLE_0:3; :: thesis: verum
end;
suppose A41: Y in Z5 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9, YA being set such that
A42: ( 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
A43: YA in Y and
A44: Y1 meets X by A10;
Y in union (union (union (union (union X)))) by A10, A41;
then YA in union (union (union (union (union (union X))))) by A43, TARSKI:def 4;
then YA in Z6 by A8, A42, A44;
then YA in (((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6 by XBOOLE_0:def 3;
then YA in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
then YA in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_0:def 3;
then YA in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then YA in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
then YA in ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB by XBOOLE_0:def 3;
then YA in (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_0:def 3;
then YA in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_0:def 3;
then YA in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then YA in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A43, XBOOLE_0:3; :: thesis: verum
end;
suppose A45: Y in Z6 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8, Y9 being set such that
A46: ( 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
A47: Y9 in Y and
A48: Y1 meets X by A8;
Y in union (union (union (union (union (union X))))) by A8, A45;
then Y9 in union (union (union (union (union (union (union X)))))) by A47, TARSKI:def 4;
then Y9 in Z7 by A7, A46, A48;
then Y9 in ((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7 by XBOOLE_0:def 3;
then Y9 in (((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8 by XBOOLE_0:def 3;
then Y9 in ((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9 by XBOOLE_0:def 3;
then Y9 in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
then Y9 in ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB by XBOOLE_0:def 3;
then Y9 in (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_0:def 3;
then Y9 in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_0:def 3;
then Y9 in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then Y9 in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A47, XBOOLE_0:3; :: thesis: verum
end;
suppose A49: Y in Z7 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7, Y8 being set such that
A50: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 ) and
A51: Y8 in Y and
A52: Y1 meets X by A7;
Y in union (union (union (union (union (union (union X)))))) by A7, A49;
then Y8 in union (union (union (union (union (union (union (union X))))))) by A51, TARSKI:def 4;
then Y8 in Z8 by A4, A50, A52;
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;
then Y8 in ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB by XBOOLE_0:def 3;
then Y8 in (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_0:def 3;
then Y8 in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_0:def 3;
then Y8 in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then Y8 in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A51, XBOOLE_0:3; :: thesis: verum
end;
suppose A53: Y in Z8 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6, Y7 being set such that
A54: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 ) and
A55: Y7 in Y and
A56: Y1 meets X by A4;
Y in union (union (union (union (union (union (union (union X))))))) by A4, A53;
then Y7 in union (union (union (union (union (union (union (union (union X)))))))) by A55, TARSKI:def 4;
then Y7 in Z9 by A3, A54, A56;
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;
then Y7 in ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB by XBOOLE_0:def 3;
then Y7 in (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_0:def 3;
then Y7 in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_0:def 3;
then Y7 in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then Y7 in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A55, XBOOLE_0:3; :: thesis: verum
end;
suppose A57: Y in Z9 ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5, Y6 being set such that
A58: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 ) and
A59: Y6 in Y and
A60: Y1 meets X by A3;
Y in union (union (union (union (union (union (union (union (union X)))))))) by A3, A57;
then Y6 in union (union (union (union (union (union (union (union (union (union X))))))))) by A59, TARSKI:def 4;
then Y6 in ZA by A15, A58, A60;
then Y6 in (((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA by XBOOLE_0:def 3;
then Y6 in ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB by XBOOLE_0:def 3;
then Y6 in (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_0:def 3;
then Y6 in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_0:def 3;
then Y6 in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then Y6 in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A59, XBOOLE_0:3; :: thesis: verum
end;
suppose A61: Y in ZA ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4, Y5 being set such that
A62: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 ) and
A63: Y5 in Y and
A64: Y1 meets X by A15;
Y in union (union (union (union (union (union (union (union (union (union X))))))))) by A15, A61;
then Y5 in union (union (union (union (union (union (union (union (union (union (union X)))))))))) by A63, TARSKI:def 4;
then Y5 in ZB by A14, A62, A64;
then Y5 in ((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB by XBOOLE_0:def 3;
then Y5 in (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_0:def 3;
then Y5 in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_0:def 3;
then Y5 in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then Y5 in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A63, XBOOLE_0:3; :: thesis: verum
end;
suppose A65: Y in ZB ; :: thesis: contradiction
then consider Y1, Y2, Y3, Y4 being set such that
A66: ( Y1 in Y2 & Y2 in Y3 & Y3 in Y4 ) and
A67: Y4 in Y and
A68: Y1 meets X by A14;
Y in union (union (union (union (union (union (union (union (union (union (union X)))))))))) by A14, A65;
then Y4 in union (union (union (union (union (union (union (union (union (union (union (union X))))))))))) by A67, TARSKI:def 4;
then Y4 in ZC by A13, A66, A68;
then Y4 in (((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC by XBOOLE_0:def 3;
then Y4 in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_0:def 3;
then Y4 in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then Y4 in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A67, XBOOLE_0:3; :: thesis: verum
end;
suppose A69: Y in ZC ; :: thesis: contradiction
then consider Y1, Y2, Y3 being set such that
A70: ( Y1 in Y2 & Y2 in Y3 ) and
A71: Y3 in Y and
A72: Y1 meets X by A13;
Y in union (union (union (union (union (union (union (union (union (union (union (union X))))))))))) by A13, A69;
then Y3 in union (union (union (union (union (union (union (union (union (union (union (union (union X)))))))))))) by A71, TARSKI:def 4;
then Y3 in ZD by A12, A70, A72;
then Y3 in ((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD by XBOOLE_0:def 3;
then Y3 in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then Y3 in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A71, XBOOLE_0:3; :: thesis: verum
end;
suppose A73: Y in ZD ; :: thesis: contradiction
then consider Y1, Y2 being set such that
A74: Y1 in Y2 and
A75: Y2 in Y and
A76: Y1 meets X by A12;
Y in union (union (union (union (union (union (union (union (union (union (union (union (union X)))))))))))) by A12, A73;
then Y2 in union (union (union (union (union (union (union (union (union (union (union (union (union (union X))))))))))))) by A75, TARSKI:def 4;
then Y2 in ZE by A9, A74, A76;
then Y2 in (((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE by XBOOLE_0:def 3;
then Y2 in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A75, XBOOLE_0:3; :: thesis: verum
end;
suppose A77: Y in ZE ; :: thesis: contradiction
then consider Y1 being set such that
A78: Y1 in Y and
A79: Y1 meets X by A9;
Y in union (union (union (union (union (union (union (union (union (union (union (union (union (union X))))))))))))) by A9, A77;
then Y1 in union (union (union (union (union (union (union (union (union (union (union (union (union (union (union X)))))))))))))) by A78, TARSKI:def 4;
then Y1 in ZF by A5, A79;
then Y1 in ((((((((((((((X \/ Z1) \/ Z2) \/ Z3) \/ Z4) \/ Z5) \/ Z6) \/ Z7) \/ Z8) \/ Z9) \/ ZA) \/ ZB) \/ ZC) \/ ZD) \/ ZE) \/ ZF by XBOOLE_0:def 3;
hence contradiction by A18, A78, XBOOLE_0:3; :: thesis: verum
end;
suppose Y in ZF ; :: thesis: contradiction
then Y meets X by A5;
hence contradiction by A16, A18, XBOOLE_1:70; :: thesis: verum
end;
end;