### The Mizar article:

### $N$-Tuples and Cartesian Products for $n=8$

**by****Michal Muzalewski, and****Wojciech Skaba**

- Received October 15, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: MCART_5
- [ MML identifier index ]

environ vocabulary BOOLE, TARSKI, MCART_1, MCART_2, MCART_3, MCART_4, MCART_5; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, MCART_2, MCART_3, MCART_4; constructors TARSKI, MCART_1, MCART_2, MCART_3, MCART_4, MEMBERED, XBOOLE_0; clusters MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; theorems TARSKI, ZFMISC_1, MCART_1, MCART_2, MCART_3, MCART_4, XBOOLE_0, XBOOLE_1; schemes XBOOLE_0; begin reserve x1,x2,x3,x4,x5,x6,x7,x8 for set; reserve y,y1,y2,y3,y4,y5,y6,y7,y8 for set; reserve X,X1,X2,X3,X4,X5,X6,X7,X8 for set; reserve Y,Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD for set; reserve Z,Z1,Z2,Z3,Z4,Z5,Z6,Z7,Z8,Z9,ZA,ZB,ZC,ZD for set; reserve xx1 for Element of X1; reserve xx2 for Element of X2; reserve xx3 for Element of X3; reserve xx4 for Element of X4; reserve xx5 for Element of X5; reserve xx6 for Element of X6; reserve xx7 for Element of X7; theorem X <> {} implies ex Y st Y in X & for Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC 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 Y holds Y1 misses X proof defpred P1[set] means ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB 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; consider Z1 such that A1: for Y holds Y in Z1 iff Y in union X & P1[Y] from Separation; defpred P2[set] means ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA 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; consider Z2 such that A2: for Y holds Y in Z2 iff Y in union union X & P2[Y] from Separation; defpred P3[set] means ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9 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 Z3 such that A3: for Y holds Y in Z3 iff Y in union union union X & P3[Y] from Separation; defpred P4[set] means ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8 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 Z4 such that A4: for Y holds Y in Z4 iff Y in union union union union X & P4[Y] from Separation; defpred P5[set] means ex Y1,Y2,Y3,Y4,Y5,Y6,Y7 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; consider Z5 such that A5: for Y holds Y in Z5 iff Y in union union union union union X & P5[Y] from Separation; defpred P6[set] means ex Y1,Y2,Y3,Y4,Y5,Y6 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in $1 & Y1 meets X; consider Z6 such that A6: for Y holds Y in Z6 iff Y in union union union union union union X & P6[Y] from Separation; defpred P7[set] means ex Y1,Y2,Y3,Y4,Y5 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in $1 & Y1 meets X; consider Z7 such that A7: for Y holds Y in Z7 iff Y in union union union union union union union X & P7[Y] from Separation; defpred P8[set] means ex Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in $1 & Y1 meets X; consider Z8 such that A8: for Y holds Y in Z8 iff Y in union union union union union union union union X & P8[Y] from Separation; defpred P9[set] means ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X; consider Z9 such that A9: for Y holds Y in Z9 iff Y in union union union union union union union union union X & P9[Y] from Separation; defpred P10[set] means ex Y1,Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X; consider ZA such that A10: for Y holds Y in ZA iff Y in union union union union union union union union union union X & P10[Y] from Separation; defpred P11[set] means ex Y1 st Y1 in $1 & Y1 meets X; consider ZB such that A11: for Y holds Y in ZB iff Y in union union union union union union union union union union (union X) & P11[Y] from Separation; defpred P12[set] means $1 meets X; consider ZC such that A12: for Y holds Y in ZC iff Y in union union union union union union union union union union (union union X) & P12[Y] from Separation; set V = (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC; A13: V = (X \/ (Z1 \/ Z2)) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7) \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8) \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9) \/ ZA \/ ZB \/ ZC by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA) \/ ZB \/ ZC by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB) \/ ZC by XBOOLE_1:4 .= X \/ ((Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC) by XBOOLE_1:4; assume X <> {}; then V <> {} by A13,XBOOLE_1:15; then consider Y such that A14: Y in V and A15: Y misses V by MCART_1:1; assume A16: not thesis; Y in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB or Y in ZC by A14,XBOOLE_0:def 2; then Y in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA or Y in ZB or Y in ZC by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; then A17: 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 by XBOOLE_0:def 2; per cases by A17,XBOOLE_0:def 2; suppose A18: Y in X; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC such that A19: 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 Y & not Y1 misses X by A16; YC in union X & Y1 meets X by A18,A19,TARSKI:def 4; then YC in Z1 by A1,A19; then YC in X \/ Z1 by XBOOLE_0:def 2; then YC in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then YC in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then YC in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by A19,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; hence contradiction by A15,XBOOLE_1:70; suppose A20: Y in Z1; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB 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 & YA in YB & YB in Y & Y1 meets X by A1; Y in union X by A1,A20; then YB in union union X by A21,TARSKI:def 4; then YB in Z2 by A2,A21; then YB in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 by A21,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; hence contradiction by A15,XBOOLE_1:70; suppose A22: Y in Z2; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA such that A23: 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 & Y1 meets X by A2; Y in union union X by A2,A22; then YA in union union union X by A23,TARSKI:def 4; then YA in Z3 by A3,A23; then YA in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then YA in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then YA in V by XBOOLE_0:def 2; hence contradiction by A15,A23,XBOOLE_0:3; suppose A24: Y in Z3; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9 such that A25: 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 Y & Y1 meets X by A3; Y in union union union X by A3,A24; then Y9 in union union union union X by A25,TARSKI:def 4; then Y9 in Z4 by A4,A25; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y9 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y9 in V by XBOOLE_0:def 2; hence contradiction by A15,A25,XBOOLE_0:3; suppose A26: Y in Z4; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8 such that A27: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y8 & Y8 in Y & Y1 meets X by A4; Y in union union union union X by A4,A26; then Y8 in union union union union union X by A27,TARSKI:def 4; then Y8 in Z5 by A5,A27; then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2; then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y8 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y8 in V by XBOOLE_0:def 2; hence contradiction by A15,A27,XBOOLE_0:3; suppose A28: Y in Z5; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7 such that A29: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y & Y1 meets X by A5; Y in union union union union union X by A5,A28; then Y7 in union union union union union union X by A29,TARSKI:def 4; then Y7 in Z6 by A6,A29; then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2; then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y7 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y7 in V by XBOOLE_0:def 2; hence contradiction by A15,A29,XBOOLE_0:3; suppose A30: Y in Z6; then consider Y1,Y2,Y3,Y4,Y5,Y6 such that A31: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y & Y1 meets X by A6; Y in union union union union union union X by A6,A30; then Y6 in union union union union union union union X by A31,TARSKI:def 4; then Y6 in Z7 by A7,A31; then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2; then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y6 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y6 in V by XBOOLE_0:def 2; hence contradiction by A15,A31,XBOOLE_0:3; suppose A32: Y in Z7; then consider Y1,Y2,Y3,Y4,Y5 such that A33: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y & Y1 meets X by A7; Y in union union union union union union union X by A7,A32; then Y5 in union union union union union union union union X by A33,TARSKI:def 4; then Y5 in Z8 by A8,A33; then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y5 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y5 in V by XBOOLE_0:def 2; hence contradiction by A15,A33,XBOOLE_0:3; suppose A34: Y in Z8; then consider Y1,Y2,Y3,Y4 such that A35: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & Y1 meets X by A8; Y in union union union union union union union union X by A8,A34; then Y4 in union union union union union union union union union X by A35,TARSKI:def 4; then Y4 in Z9 by A9,A35; then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y4 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y4 in V by XBOOLE_0:def 2; hence contradiction by A15,A35,XBOOLE_0:3; suppose A36: Y in Z9; then consider Y1,Y2,Y3 such that A37: Y1 in Y2 & Y2 in Y3 & Y3 in Y & Y1 meets X by A9; Y in union union union union union union union union union X by A9,A36; then Y3 in union union union union union union union union union union X by A37,TARSKI:def 4; then Y3 in ZA by A10,A37; then Y3 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y3 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y3 in V by XBOOLE_0:def 2; hence contradiction by A15,A37,XBOOLE_0:3; suppose A38: Y in ZA; then consider Y1,Y2 such that A39: Y1 in Y2 & Y2 in Y & Y1 meets X by A10; Y in union union union union union union union union union union X by A10,A38; then Y2 in union union union union union union union union union union (union X) by A39,TARSKI:def 4; then Y2 in ZB by A11,A39; then Y2 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y2 in V by XBOOLE_0:def 2; hence contradiction by A15,A39,XBOOLE_0:3; suppose A40: Y in ZB; then consider Y1 such that A41: Y1 in Y & Y1 meets X by A11; Y in union union union union union union union union union union (union X ) by A11,A40; then Y1 in union union union union union union union union union union (union union X) by A41,TARSKI:def 4; then Y1 in ZC by A12,A41; then Y1 in V by XBOOLE_0:def 2; hence contradiction by A15,A41,XBOOLE_0:3; suppose Y in ZC; then Y meets X by A12; hence contradiction by A13,A15,XBOOLE_1:70; end; theorem Th2: X <> {} implies ex Y st Y in X & for Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD 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 Y holds Y1 misses X proof defpred P1[set] means ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC 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; consider Z1 such that A1: for Y holds Y in Z1 iff Y in union X & P1[Y] from Separation; defpred P2[set] means ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB 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; consider Z2 such that A2: for Y holds Y in Z2 iff Y in union union X & P2[Y] from Separation; defpred P3[set] means ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA 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; consider Z3 such that A3: for Y holds Y in Z3 iff Y in union union union X & P3[Y] from Separation; defpred P4[set] means ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9 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 Z4 such that A4: for Y holds Y in Z4 iff Y in union union union union X & P4[Y] from Separation; defpred P5[set] means ex Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8 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 Z5 such that A5: for Y holds Y in Z5 iff Y in union union union union union X & P5[Y] from Separation; defpred P6[set] means ex Y1,Y2,Y3,Y4,Y5,Y6,Y7 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; consider Z6 such that A6: for Y holds Y in Z6 iff Y in union union union union union union X & P6[Y] from Separation; defpred P7[set] means ex Y1,Y2,Y3,Y4,Y5,Y6 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in $1 & Y1 meets X; consider Z7 such that A7: for Y holds Y in Z7 iff Y in union union union union union union union X & P7[Y] from Separation; defpred P8[set] means ex Y1,Y2,Y3,Y4,Y5 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in $1 & Y1 meets X; consider Z8 such that A8: for Y holds Y in Z8 iff Y in union union union union union union union union X & P8[Y] from Separation; defpred P9[set] means ex Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in $1 & Y1 meets X; consider Z9 such that A9: for Y holds Y in Z9 iff Y in union union union union union union union union union X & P9[Y] from Separation; defpred P10[set] means ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in $1 & Y1 meets X; consider ZA such that A10: for Y holds Y in ZA iff Y in union union union union union union union union union union X & P10[Y] from Separation; defpred P11[set] means ex Y1,Y2 st Y1 in Y2 & Y2 in $1 & Y1 meets X; consider ZB such that A11: for Y holds Y in ZB iff Y in union union union union union union union union union union (union X) & P11[Y] from Separation; defpred P12[set] means ex Y1 st Y1 in $1 & Y1 meets X; consider ZC such that A12: for Y holds Y in ZC iff Y in union union union union union union union union union union (union union X) & P12[Y] from Separation; defpred P13[set] means $1 meets X; consider ZD such that A13: for Y holds Y in ZD iff Y in union union union union union union union union union union (union union union X) & P13[Y] from Separation; set V = (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC \/ ZD; A14: V = (X \/ (Z1 \/ Z2) \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC \/ ZD by XBOOLE_1:4 .= (X \/ (Z1 \/ Z2 \/ Z3)) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC \/ ZD by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4) \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC \/ ZD by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5) \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC \/ ZD by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6) \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC \/ ZD by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7) \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC \/ ZD by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8) \/ Z9 \/ ZA \/ ZB \/ ZC \/ ZD by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9) \/ ZA \/ ZB \/ ZC \/ ZD by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA) \/ ZB \/ ZC \/ ZD by XBOOLE_1:4 .= X \/ (Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB) \/ ZC \/ ZD by XBOOLE_1:4 .= X \/ ((Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC) \/ ZD by XBOOLE_1:4 .= X \/ ((Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC \/ ZD) by XBOOLE_1:4; assume X <> {}; then V <> {} by A14,XBOOLE_1:15; then consider Y such that A15: Y in V and A16: Y misses V by MCART_1:1; assume A17: not thesis; Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC or Y in ZD by A15,XBOOLE_0:def 2; then Y in (X \/ Z1 \/ Z2 \/ Z3) \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB or Y in ZC or Y in ZD by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; 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 by XBOOLE_0:def 2; then A18: 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 by XBOOLE_0:def 2; per cases by A18,XBOOLE_0:def 2; suppose A19: Y in X; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD such that A20: 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 Y & not Y1 misses X by A17; YD in union X & Y1 meets X by A19,A20,TARSKI:def 4; then YD in Z1 by A1,A20; then YD in X \/ Z1 by XBOOLE_0:def 2; then YD in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then YD in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; then YD in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then YD in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by A20,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; hence contradiction by A16,XBOOLE_1:70; suppose A21: Y in Z1; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC 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 Y & Y1 meets X by A1; Y in union X by A1,A21; then YC in union union X by A22,TARSKI:def 4; then YC in Z2 by A2,A22; then YC in X \/ Z1 \/ Z2 by XBOOLE_0:def 2; then Y meets X \/ Z1 \/ Z2 by A22,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; hence contradiction by A16,XBOOLE_1:70; suppose A23: Y in Z2; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB such that A24: 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 Y & Y1 meets X by A2; Y in union union X by A2,A23; then YB in union union union X by A24,TARSKI:def 4; then YB in Z3 by A3,A24; then YB in X \/ Z1 \/ Z2 \/ Z3 by XBOOLE_0:def 2; then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2; then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then YB in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then YB in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then YB in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_0:def 2; then YB in V by XBOOLE_0:def 2; hence contradiction by A16,A24,XBOOLE_0:3; suppose A25: Y in Z3; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA 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 Y & Y1 meets X by A3; Y in union union union X by A3,A25; then YA in union union union union X by A26,TARSKI:def 4; then YA in Z4 by A4,A26; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then YA in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then YA in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then YA in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_0:def 2; then YA in V by XBOOLE_0:def 2; hence contradiction by A16,A26,XBOOLE_0:3; suppose A27: Y in Z4; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9 such that A28: 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 Y & Y1 meets X by A4; Y in union union union union X by A4,A27; then Y9 in union union union union union X by A28,TARSKI:def 4; then Y9 in Z5 by A5,A28; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 by XBOOLE_0:def 2; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then Y9 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y9 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y9 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_0:def 2; then Y9 in V by XBOOLE_0:def 2; hence contradiction by A16,A28,XBOOLE_0:3; suppose A29: Y in Z5; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8 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 Y & Y1 meets X by A5; Y in union union union union union X by A5,A29; then Y8 in union union union union union union X by A30,TARSKI:def 4; then Y8 in Z6 by A6,A30; then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 by XBOOLE_0:def 2; then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2; then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then Y8 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y8 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y8 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_0:def 2; then Y8 in V by XBOOLE_0:def 2; hence contradiction by A16,A30,XBOOLE_0:3; suppose A31: Y in Z6; then consider Y1,Y2,Y3,Y4,Y5,Y6,Y7 such that A32: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in Y & Y1 meets X by A6; Y in union union union union union union X by A6,A31; then Y7 in union union union union union union union X by A32,TARSKI:def 4; then Y7 in Z7 by A7,A32; then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 by XBOOLE_0:def 2; then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then Y7 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y7 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y7 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_0:def 2; then Y7 in V by XBOOLE_0:def 2; hence contradiction by A16,A32,XBOOLE_0:3; suppose A33: Y in Z7; then consider Y1,Y2,Y3,Y4,Y5,Y6 such that A34: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y & Y1 meets X by A7; Y in union union union union union union union X by A7,A33; then Y6 in union union union union union union union union X by A34,TARSKI:def 4; then Y6 in Z8 by A8,A34; then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 by XBOOLE_0:def 2; then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then Y6 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y6 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y6 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_0:def 2; then Y6 in V by XBOOLE_0:def 2; hence contradiction by A16,A34,XBOOLE_0:3; suppose A35: Y in Z8; then consider Y1,Y2,Y3,Y4,Y5 such that A36: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y & Y1 meets X by A8; Y in union union union union union union union union X by A8,A35; then Y5 in union union union union union union union union union X by A36,TARSKI:def 4; then Y5 in Z9 by A9,A36; then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 by XBOOLE_0:def 2; then Y5 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y5 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y5 in ((X \/ Z1) \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_0:def 2; then Y5 in V by XBOOLE_0:def 2; hence contradiction by A16,A36,XBOOLE_0:3; suppose A37: Y in Z9; then consider Y1,Y2,Y3,Y4 such that A38: Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y & Y1 meets X by A9; Y in union union union union union union union union union X by A9,A37; then Y4 in union union union union union union union union union union X by A38,TARSKI:def 4; then Y4 in ZA by A10,A38; then Y4 in X \/ Z1 \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA by XBOOLE_0:def 2; then Y4 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y4 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_0:def 2; then Y4 in V by XBOOLE_0:def 2; hence contradiction by A16,A38,XBOOLE_0:3; suppose A39: Y in ZA; then consider Y1,Y2,Y3 such that A40: Y1 in Y2 & Y2 in Y3 & Y3 in Y & Y1 meets X by A10; Y in union union union union union union union union union union X by A10,A39; then Y3 in union union union union union union union union union union (union X) by A40,TARSKI:def 4; then Y3 in ZB by A11,A40; then Y3 in (X \/ Z1) \/ Z2 \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB by XBOOLE_0:def 2; then Y3 in (X \/ Z1 \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_0:def 2; then Y3 in V by XBOOLE_0:def 2; hence contradiction by A16,A40,XBOOLE_0:3; suppose A41: Y in ZB; then consider Y1,Y2 such that A42: Y1 in Y2 & Y2 in Y & Y1 meets X by A11; Y in union union union union union union union union union union (union X ) by A11,A41; then Y2 in union union union union union union union union union union (union union X) by A42,TARSKI:def 4; then Y2 in ZC by A12,A42; then Y2 in ((X \/ Z1) \/ Z2) \/ Z3 \/ Z4 \/ Z5 \/ Z6 \/ Z7 \/ Z8 \/ Z9 \/ ZA \/ ZB \/ ZC by XBOOLE_0:def 2; then Y2 in V by XBOOLE_0:def 2; hence contradiction by A16,A42,XBOOLE_0:3; suppose A43: Y in ZC; then consider Y1 such that A44: Y1 in Y & Y1 meets X by A12; Y in union union union union union union union union union union (union union X) by A12,A43; then Y1 in union union union union union union union union union union (union union union X) by A44,TARSKI:def 4; then Y1 in ZD by A13,A44; then Y1 in V by XBOOLE_0:def 2; hence contradiction by A16,A44,XBOOLE_0:3; suppose Y in ZD; then Y meets X by A13; hence contradiction by A14,A16,XBOOLE_1:70; end; :: :: Tuples for n=8 :: definition let x1,x2,x3,x4,x5,x6,x7,x8; func [x1,x2,x3,x4,x5,x6,x7,x8] equals :Def1: [[x1,x2,x3,x4,x5,x6,x7],x8]; correctness; end; theorem Th3: [x1,x2,x3,x4,x5,x6,x7,x8] = [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8] proof thus [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4,x5,x6,x7],x8] by Def1 .= [[[x1,x2,x3,x4,x5,x6],x7],x8] by MCART_4:def 1 .= [[[[x1,x2,x3,x4,x5],x6],x7],x8] by MCART_3:def 1 .= [[[[[x1,x2,x3,x4],x5],x6],x7],x8] by MCART_2:def 1 .= [[[[[[x1,x2,x3],x4],x5],x6],x7],x8] by MCART_1:def 4 .= [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8] by MCART_1:def 3; end; canceled; theorem [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4,x5,x6],x7,x8] proof thus [x1,x2,x3,x4,x5,x6,x7,x8] = [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8] by Th3 .= [[[[[[x1,x2],x3],x4],x5],x6],x7,x8] by MCART_1:def 3 .= [[x1,x2,x3,x4,x5,x6],x7,x8] by MCART_3:3; end; theorem [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4,x5],x6,x7,x8] proof thus [x1,x2,x3,x4,x5,x6,x7,x8] = [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8] by Th3 .= [[[[[x1,x2],x3],x4],x5],x6,x7,x8] by MCART_1:31 .= [[x1,x2,x3,x4,x5],x6,x7,x8] by MCART_2:3; end; theorem [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4],x5,x6,x7,x8] proof thus [x1,x2,x3,x4,x5,x6,x7,x8] = [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8] by Th3 .= [[[[x1,x2],x3],x4],x5,x6,x7,x8] by MCART_2:3 .= [[x1,x2,x3,x4],x5,x6,x7,x8] by MCART_1:31; end; theorem [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3],x4,x5,x6,x7,x8] proof thus [x1,x2,x3,x4,x5,x6,x7,x8] = [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8] by Th3 .= [[[x1,x2],x3],x4,x5,x6,x7,x8] by MCART_3:3 .= [[x1,x2,x3],x4,x5,x6,x7,x8] by MCART_1:def 3; end; theorem Th9: [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2],x3,x4,x5,x6,x7,x8] proof thus [x1,x2,x3,x4,x5,x6,x7,x8] = [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8] by Th3 .= [[[x1,x2],x3],x4,x5,x6,x7,x8] by MCART_3:3 .= [[x1,x2],x3,x4,x5,x6,x7,x8] by MCART_4:8; end; theorem Th10: [x1,x2,x3,x4,x5,x6,x7,x8] = [y1,y2,y3,y4,y5,y6,y7,y8] implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6 & x7 = y7 & x8 = y8 proof assume [x1,x2,x3,x4,x5,x6,x7,x8] = [y1,y2,y3,y4,y5,y6,y7,y8]; then [[x1,x2,x3,x4,x5,x6,x7],x8] = [y1,y2,y3,y4,y5,y6,y7,y8] by Def1 .= [[y1,y2,y3,y4,y5,y6,y7],y8] by Def1; then [x1,x2,x3,x4,x5,x6,x7] = [y1,y2,y3,y4,y5,y6,y7] & x8 = y8 by ZFMISC_1:33; hence thesis by MCART_4:9; end; theorem Th11: X <> {} implies ex y st y in X & not ex x1,x2,x3,x4,x5,x6,x7,x8 st (x1 in X or x2 in X) & y = [x1,x2,x3,x4,x5,x6,x7,x8] proof assume X <> {}; then consider Y such that A1: Y in X and A2: for Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD 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 Y holds Y1 misses X by Th2; take y = Y; thus y in X by A1; given x1,x2,x3,x4,x5,x6,x7,x8 such that A3: x1 in X or x2 in X and A4: y = [x1,x2,x3,x4,x5,x6,x7,x8]; set Y1 = { x1, x2 }, Y2 = { Y1, {x1} }, Y3 = { Y2, x3 }, Y4 = { Y3, {Y2} }, Y5 = { Y4, x4 }, Y6 = { Y5, {Y4} }, Y7 = { Y6, x5 }, Y8 = { Y7, {Y6} }, Y9 = { Y8, x6 }, YA = { Y9, {Y8} }, YB = { YA, x7 }, YC = { YB, {YA} }, YD = { YC, x8 }; x1 in Y1 & x2 in Y1 by TARSKI:def 2; then A5: not Y1 misses X by A3,XBOOLE_0:3; Y = [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8] by A4,Th3 .= [[[[[[ Y2,x3],x4],x5],x6],x7],x8 ] by TARSKI:def 5 .= [[[[[ Y4,x4],x5],x6],x7],x8 ] by TARSKI:def 5 .= [[[[ Y6,x5 ],x6],x7],x8 ] by TARSKI:def 5 .= [[[ Y8,x6],x7],x8 ] by TARSKI:def 5 .= [[ YA,x7],x8 ] by TARSKI:def 5 .= [ YC,x8 ] by TARSKI:def 5 .= { YD, { YC } } by TARSKI:def 5; then 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 Y by TARSKI:def 2; hence contradiction by A2,A5; end; :: :: Cartesian products of eight sets :: definition let X1,X2,X3,X4,X5,X6,X7,X8; func [:X1,X2,X3,X4,X5,X6,X7,X8:] -> set equals :Def2: [:[: X1,X2,X3,X4,X5,X6,X7 :],X8 :]; correctness; end; theorem Th12: [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:] proof thus [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4,X5,X6,X7:],X8:] by Def2 .= [:[:[:X1,X2,X3,X4,X5,X6:],X7:],X8:] by MCART_4:def 2 .= [:[:[:[:X1,X2,X3,X4,X5:],X6:],X7:],X8:] by MCART_3:def 2 .= [:[:[:[:[:X1,X2,X3,X4:],X5:],X6:],X7:],X8:] by MCART_2:def 2 .= [:[:[:[:[:[:X1,X2,X3:],X4:],X5:],X6:],X7:],X8:] by ZFMISC_1:def 4 .= [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:] by ZFMISC_1:def 3; end; canceled; theorem [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4,X5,X6:],X7,X8:] proof thus [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:] by Th12 .= [:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7,X8:] by ZFMISC_1:def 3 .= [:[:X1,X2,X3,X4,X5,X6:],X7,X8:] by MCART_3:10; end; theorem [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4,X5:],X6,X7,X8:] proof thus [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:] by Th12 .= [:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6,X7,X8:] by MCART_1:53 .= [:[:X1,X2,X3,X4,X5:],X6,X7,X8:] by MCART_2:9; end; theorem [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4:],X5,X6,X7,X8:] proof thus [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:] by Th12 .= [:[:[:[:X1,X2:],X3:],X4:],X5,X6,X7,X8:] by MCART_2:9 .= [:[:X1,X2,X3,X4:],X5,X6,X7,X8:] by MCART_1:53; end; theorem [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3:],X4,X5,X6,X7,X8:] proof thus [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:] by Th12 .= [:[:[:X1,X2:],X3:],X4,X5,X6,X7,X8:] by MCART_3:10 .= [:[:X1,X2,X3:],X4,X5,X6,X7,X8:] by ZFMISC_1:def 3; end; theorem Th18: [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2:],X3,X4,X5,X6,X7,X8:] proof thus [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:] by Th12 .= [:[:[:X1,X2:],X3:],X4,X5,X6,X7,X8:] by MCART_3:10 .= [:[:X1,X2:],X3,X4,X5,X6,X7,X8:] by MCART_4:16; end; theorem Th19: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} & X8 <> {} iff [:X1,X2,X3,X4,X5,X6,X7,X8:] <> {} proof A1: [:[:X1,X2,X3,X4,X5,X6,X7:],X8:] = [:X1,X2,X3,X4,X5,X6,X7,X8:] by Def2; X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {} & X7 <> {} iff [:X1,X2,X3,X4,X5,X6,X7:] <> {} by MCART_4:17; hence thesis by A1,ZFMISC_1:113; end; theorem Th20: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} implies ( [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 & X6=Y6 & X7=Y7 & X8=Y8) proof A1: [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4,X5,X6,X7:],X8:] by Def2; assume A2: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{}; then A3: [:X1,X2,X3,X4,X5,X6,X7:] <> {} by MCART_4:17; assume A4: X8<>{}; assume [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:]; then [:[:X1,X2,X3,X4,X5,X6,X7:],X8:] = [:[:Y1,Y2,Y3,Y4,Y5,Y6,Y7:],Y8:] by A1,Def2; then [:X1,X2,X3,X4,X5,X6,X7:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] & X8 = Y8 by A3,A4,ZFMISC_1:134; hence thesis by A2,MCART_4:18; end; theorem [:X1,X2,X3,X4,X5,X6,X7,X8:]<>{} & [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 & X6=Y6 & X7=Y7 & X8=Y8 proof assume [:X1,X2,X3,X4,X5,X6,X7,X8:]<>{}; then X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<> {} by Th19; hence thesis by Th20; end; theorem [:X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y:] implies X = Y proof assume [:X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y:]; then X<>{} or Y<>{} implies thesis by Th20; hence X = Y; end; reserve xx8 for Element of X8; theorem Th23: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} implies for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] ex xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] proof assume A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}; then A2: [:X1,X2,X3,X4,X5,X6,X7:] <> {} by MCART_4:17; let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]; reconsider x'=x as Element of [:[:X1,X2,X3,X4,X5,X6,X7:],X8:] by Def2; consider x1234567 being (Element of [:X1,X2,X3,X4,X5,X6,X7:]), xx8 such that A3: x' = [x1234567,xx8] by A1,A2,MCART_2:36; consider xx1,xx2,xx3,xx4,xx5,xx6,xx7 such that A4: x1234567 = [xx1,xx2,xx3,xx4,xx5,xx6,xx7] by A1,MCART_4:21; take xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8; thus x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A3,A4,Def1; end; definition let X1,X2,X3,X4,X5,X6,X7,X8; assume A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}; let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]; func x`1 -> Element of X1 means :Def3: x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x1; existence proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A2: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; take xx1; thus thesis by A2,Th10; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A3: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; let y,z be Element of X1; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies y = x1; then A4: y = xx1 by A3; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies z = x1; hence thesis by A3,A4; end; func x`2 -> Element of X2 means :Def4: x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x2; existence proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A5: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; take xx2; thus thesis by A5,Th10; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A6: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; let y,z be Element of X2; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies y = x2; then A7: y = xx2 by A6; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies z = x2; hence thesis by A6,A7; end; func x`3 -> Element of X3 means :Def5: x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x3; existence proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A8: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; take xx3; thus thesis by A8,Th10; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A9: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; let y,z be Element of X3; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies y = x3; then A10: y = xx3 by A9; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies z = x3; hence thesis by A9,A10; end; func x`4 -> Element of X4 means :Def6: x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x4; existence proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A11: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; take xx4; thus thesis by A11,Th10; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A12: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; let y,z be Element of X4; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies y = x4; then A13: y = xx4 by A12; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies z = x4; hence thesis by A12,A13; end; func x`5 -> Element of X5 means :Def7: x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x5; existence proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A14: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; take xx5; thus thesis by A14,Th10; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A15: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; let y,z be Element of X5; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies y = x5; then A16: y = xx5 by A15; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies z = x5; hence thesis by A15,A16; end; func x`6 -> Element of X6 means :Def8: x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x6; existence proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A17: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; take xx6; thus thesis by A17,Th10; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A18: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; let y,z be Element of X6; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies y = x6; then A19: y = xx6 by A18; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies z = x6; hence thesis by A18,A19; end; func x`7 -> Element of X7 means :Def9: x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x7; existence proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A20: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; take xx7; thus thesis by A20,Th10; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A21: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; let y,z be Element of X7; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies y = x7; then A22: y = xx7 by A21; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies z = x7; hence thesis by A21,A22; end; func x`8 -> Element of X8 means :Def10: x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x8; existence proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A23: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; take xx8; thus thesis by A23,Th10; end; uniqueness proof consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A24: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; let y,z be Element of X8; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies y = x8; then A25: y = xx8 by A24; assume x = [x1,x2,x3,x4,x5,x6,x7,x8] implies z = x8; hence thesis by A24,A25; end; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} implies for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] for x1,x2,x3,x4,x5,x6,x7,x8 st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 & x`5 = x5 & x`6 = x6 & x`7 = x7 & x`8 =x8 by Def3,Def4,Def5,Def6,Def7,Def8,Def9,Def10; theorem Th25: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} implies for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] holds x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8] proof assume A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}; let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]; consider xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 such that A2: x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,Th23; thus x = [x`1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,A2,Def3 .= [x`1,x`2,xx3,xx4,xx5,xx6,xx7,xx8] by A1,A2,Def4 .= [x`1,x`2,x`3,xx4,xx5,xx6,xx7,xx8] by A1,A2,Def5 .= [x`1,x`2,x`3,x`4,xx5,xx6,xx7,xx8] by A1,A2,Def6 .= [x`1,x`2,x`3,x`4,x`5,xx6,xx7,xx8] by A1,A2,Def7 .= [x`1,x`2,x`3,x`4,x`5,x`6,xx7,xx8] by A1,A2,Def8 .= [x`1,x`2,x`3,x`4,x`5,x`6,x`7,xx8] by A1,A2,Def9 .= [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8] by A1,A2,Def10; end; theorem Th26: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} implies for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] holds x`1 = (x qua set)`1`1`1`1`1`1`1 & x`2 = (x qua set)`1`1`1`1`1`1`2 & x`3 = (x qua set)`1`1`1`1`1`2 & x`4 = (x qua set)`1`1`1`1`2 & x`5 = (x qua set)`1`1`1`2 & x`6 = (x qua set)`1`1`2 & x`7 = (x qua set)`1`2 & x`8 = (x qua set)`2 proof assume A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}; let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]; thus x`1 = [ x`1, x`2]`1 by MCART_1:7 .= [[x`1, x`2],x`3]`1`1 by MCART_1:7 .= [ x`1, x`2 ,x`3]`1`1 by MCART_1:def 3 .= [[x`1, x`2 ,x`3],x`4]`1`1`1 by MCART_1:7 .= [ x`1, x`2 ,x`3 ,x`4]`1`1`1 by MCART_1:def 4 .= [[x`1, x`2 ,x`3 ,x`4], x`5]`1`1`1`1 by MCART_1:7 .= [ x`1, x`2 ,x`3 ,x`4 , x`5]`1`1`1`1 by MCART_2:def 1 .= [[x`1, x`2 ,x`3 ,x`4, x`5],x`6]`1`1`1`1`1 by MCART_1:7 .= [ x`1, x`2 ,x`3 ,x`4 ,x`5, x`6]`1`1`1`1`1 by MCART_3:def 1 .= [[x`1, x`2 ,x`3 ,x`4, x`5, x`6],x`7]`1`1`1`1`1`1 by MCART_1:7 .= [ x`1, x`2 ,x`3 ,x`4 ,x`5, x`6, x`7]`1`1`1`1`1`1 by MCART_4:def 1 .= [[x`1, x`2 ,x`3 ,x`4, x`5, x`6, x`7],x`8]`1`1`1`1`1`1`1 by MCART_1:7 .= [ x`1, x`2 ,x`3 ,x`4 ,x`5, x`6, x`7, x`8]`1`1`1`1`1`1`1 by Def1 .= (x qua set)`1`1`1`1`1`1`1 by A1,Th25; thus x`2 = [ x`1, x`2]`2 by MCART_1:7 .= [[x`1, x`2],x`3]`1`2 by MCART_1:7 .= [ x`1, x`2, x`3]`1`2 by MCART_1:def 3 .= [[x`1, x`2, x`3],x`4]`1`1`2 by MCART_1:7 .= [ x`1, x`2, x`3, x`4]`1`1`2 by MCART_1:def 4 .= [[x`1, x`2, x`3, x`4 ], x`5]`1`1`1`2 by MCART_1:7 .= [ x`1, x`2, x`3, x`4 , x`5]`1`1`1`2 by MCART_2:def 1 .= [[x`1, x`2, x`3, x`4, x`5],x`6]`1`1`1`1`2 by MCART_1:7 .= [ x`1, x`2, x`3, x`4, x`5, x`6]`1`1`1`1`2 by MCART_3:def 1 .= [[x`1, x`2, x`3, x`4, x`5, x`6],x`7]`1`1`1`1`1`2 by MCART_1:7 .= [ x`1, x`2, x`3, x`4, x`5, x`6, x`7]`1`1`1`1`1`2 by MCART_4:def 1 .= [[x`1, x`2, x`3, x`4, x`5, x`6, x`7],x`8]`1`1`1`1`1`1`2 by MCART_1:7 .= [ x`1, x`2, x`3, x`4, x`5, x`6, x`7, x`8]`1`1`1`1`1`1`2 by Def1 .= (x qua set)`1`1`1`1`1`1`2 by A1,Th25; thus x`3 = [[x`1, x`2],x`3]`2 by MCART_1:7 .= [ x`1, x`2, x`3]`2 by MCART_1:def 3 .= [[x`1, x`2, x`3],x`4]`1`2 by MCART_1:7 .= [ x`1, x`2, x`3, x`4]`1`2 by MCART_1:def 4 .= [[x`1, x`2, x`3, x`4],x`5]`1`1`2 by MCART_1:7 .= [ x`1, x`2, x`3, x`4 ,x`5]`1`1`2 by MCART_2:def 1 .= [[x`1, x`2, x`3, x`4, x`5],x`6]`1`1`1`2 by MCART_1:7 .= [ x`1, x`2, x`3, x`4, x`5, x`6]`1`1`1`2 by MCART_3:def 1 .= [[x`1, x`2, x`3, x`4, x`5, x`6],x`7]`1`1`1`1`2 by MCART_1:7 .= [ x`1, x`2, x`3, x`4, x`5, x`6, x`7]`1`1`1`1`2 by MCART_4:def 1 .= [[x`1, x`2, x`3, x`4, x`5, x`6, x`7],x`8]`1`1`1`1`1`2 by MCART_1:7 .= [ x`1, x`2, x`3, x`4, x`5, x`6, x`7, x`8]`1`1`1`1`1`2 by Def1 .= (x qua set)`1`1`1`1`1`2 by A1,Th25; thus x`4 = [[x`1,x`2,x`3],x`4]`2 by MCART_1:7 .= [ x`1,x`2,x`3, x`4]`2 by MCART_1:def 4 .= [[x`1,x`2,x`3, x`4],x`5]`1`2 by MCART_1:7 .= [ x`1,x`2,x`3, x`4 ,x`5]`1`2 by MCART_2:def 1 .= [[x`1,x`2,x`3, x`4, x`5],x`6]`1`1`2 by MCART_1:7 .= [ x`1,x`2,x`3, x`4, x`5, x`6]`1`1`2 by MCART_3:def 1 .= [[x`1,x`2,x`3, x`4, x`5, x`6],x`7]`1`1`1`2 by MCART_1:7 .= [ x`1,x`2,x`3, x`4, x`5, x`6, x`7]`1`1`1`2 by MCART_4:def 1 .= [[x`1,x`2,x`3, x`4, x`5, x`6, x`7],x`8]`1`1`1`1`2 by MCART_1:7 .= [ x`1,x`2,x`3, x`4, x`5, x`6, x`7, x`8]`1`1`1`1`2 by Def1 .= (x qua set)`1`1`1`1`2 by A1,Th25; thus x`5 = [[x`1,x`2,x`3,x`4],x`5]`2 by MCART_1:7 .= [ x`1,x`2,x`3,x`4 ,x`5]`2 by MCART_2:def 1 .= [[x`1,x`2,x`3,x`4,x`5],x`6]`1`2 by MCART_1:7 .= [ x`1,x`2,x`3,x`4,x`5, x`6]`1`2 by MCART_3:def 1 .= [[x`1,x`2,x`3,x`4,x`5,x`6],x`7]`1`1`2 by MCART_1:7 .= [ x`1,x`2,x`3,x`4,x`5, x`6,x`7]`1`1`2 by MCART_4:def 1 .= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7],x`8]`1`1`1`2 by MCART_1:7 .= [ x`1,x`2,x`3,x`4,x`5, x`6,x`7,x`8]`1`1`1`2 by Def1 .= (x qua set)`1`1`1`2 by A1,Th25; thus x`6 = [[x`1,x`2,x`3,x`4,x`5],x`6]`2 by MCART_1:7 .= [ x`1,x`2,x`3,x`4,x`5, x`6]`2 by MCART_3:def 1 .= [[x`1,x`2,x`3,x`4,x`5,x`6],x`7]`1`2 by MCART_1:7 .= [ x`1,x`2,x`3,x`4,x`5,x`6, x`7]`1`2 by MCART_4:def 1 .= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7],x`8]`1`1`2 by MCART_1:7 .= [ x`1,x`2,x`3,x`4,x`5,x`6,x`7, x`8]`1`1`2 by Def1 .= (x qua set)`1`1`2 by A1,Th25; thus x`7 = [[x`1,x`2,x`3,x`4,x`5,x`6],x`7]`2 by MCART_1:7 .= [ x`1,x`2,x`3,x`4,x`5,x`6, x`7]`2 by MCART_4:def 1 .= [[x`1,x`2,x`3,x`4,x`5,x`6,x`7],x`8]`1`2 by MCART_1:7 .= [ x`1,x`2,x`3,x`4,x`5,x`6,x`7, x`8]`1`2 by Def1 .= (x qua set)`1`2 by A1,Th25; thus x`8 = [[x`1,x`2,x`3,x`4,x`5,x`6,x`7],x`8]`2 by MCART_1:7 .= [ x`1,x`2,x`3,x`4,x`5,x`6,x`7, x`8]`2 by Def1 .= (x qua set)`2 by A1,Th25; end; theorem X1 c= [:X1,X2,X3,X4,X5,X6,X7,X8:] or X1 c= [:X2,X3,X4,X5,X6,X7,X8,X1:] or X1 c= [:X3,X4,X5,X6,X7,X8,X1,X2:] or X1 c= [:X4,X5,X6,X7,X8,X1,X2,X3:] or X1 c= [:X5,X6,X7,X8,X1,X2,X3,X4:] or X1 c= [:X6,X7,X8,X1,X2,X3,X4,X5:] or X1 c= [:X7,X8,X1,X2,X3,X4,X5,X6:] or X1 c= [:X8,X1,X2,X3,X4,X5,X6,X7:] implies X1 = {} proof assume that A1: X1 c= [:X1,X2,X3,X4,X5,X6,X7,X8:] or X1 c= [:X2,X3,X4,X5,X6,X7,X8,X1:] or X1 c= [:X3,X4,X5,X6,X7,X8,X1,X2:] or X1 c= [:X4,X5,X6,X7,X8,X1,X2,X3:] or X1 c= [:X5,X6,X7,X8,X1,X2,X3,X4:] or X1 c= [:X6,X7,X8,X1,X2,X3,X4,X5:] or X1 c= [:X7,X8,X1,X2,X3,X4,X5,X6:] or X1 c= [:X8,X1,X2,X3,X4,X5,X6,X7:] and A2: X1 <> {}; [:X1,X2,X3,X4,X5,X6,X7,X8:]<>{} or [:X2,X3,X4,X5,X6,X7,X8,X1:]<>{} or [:X3,X4,X5,X6,X7,X8,X1,X2:]<>{} or [:X4,X5,X6,X7,X8,X1,X2,X3:]<>{} or [:X5,X6,X7,X8,X1,X2,X3,X4:]<>{} or [:X6,X7,X8,X1,X2,X3,X4,X5:]<>{} or [:X7,X8,X1,X2,X3,X4,X5,X6:]<>{} or [:X8,X1,X2,X3,X4,X5,X6,X7:]<>{} by A1,A2,XBOOLE_1:3; then A3: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} by Th19; now per cases by A1; suppose A4: X1 c= [:X1,X2,X3,X4,X5,X6,X7,X8:]; consider y such that A5: y in X1 and A6: for x1,x2,x3,x4,x5,x6,x7,x8 st x1 in X1 or x2 in X1 holds y <> [x1,x2,x3,x4,x5,x6,x7,x8] by A2,Th11; reconsider y as Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] by A4,A5; y = [y`1,y`2,y`3,y`4,y`5,y`6,y`7,y`8] & y`1 in X1 by A3,Th25; hence contradiction by A6; suppose X1 c= [:X2,X3,X4,X5,X6,X7,X8,X1:]; then X1 c= [:[:X2,X3:],X4,X5,X6,X7,X8,X1:] by Th18; hence thesis by A2,MCART_4:25; suppose X1 c= [:X3,X4,X5,X6,X7,X8,X1,X2:]; then X1 c= [:[:X3,X4:],X5,X6,X7,X8,X1,X2:] by Th18; hence thesis by A2,MCART_4:25; suppose X1 c= [:X4,X5,X6,X7,X8,X1,X2,X3:]; then X1 c= [:[:X4,X5:],X6,X7,X8,X1,X2,X3:] by Th18; hence thesis by A2,MCART_4:25; suppose X1 c= [:X5,X6,X7,X8,X1,X2,X3,X4:]; then X1 c= [:[:X5,X6:],X7,X8,X1,X2,X3,X4:] by Th18; hence thesis by A2,MCART_4:25; suppose X1 c= [:X6,X7,X8,X1,X2,X3,X4,X5:]; then X1 c= [:[:X6,X7:],X8,X1,X2,X3,X4,X5:] by Th18; hence thesis by A2,MCART_4:25; suppose X1 c= [:X7,X8,X1,X2,X3,X4,X5,X6:]; then X1 c= [:[:X7,X8:],X1,X2,X3,X4,X5,X6:] by Th18; hence thesis by A2,MCART_4:25; suppose A7: X1 c= [:X8,X1,X2,X3,X4,X5,X6,X7:]; consider y such that A8: y in X1 and A9: for x1,x2,x3,x4,x5,x6,x7,x8 st x1 in X1 or x2 in X1 holds y <> [x1,x2,x3,x4,x5,x6,x7,x8] by A2,Th11; reconsider y as Element of [:X8,X1,X2,X3,X4,X5,X6,X7:] by A7,A8; y = [y`1,y`2,y`3,y`4,y`5,y`6,y`7,y`8] & y`2 in X1 by A3,Th25; hence thesis by A9; end; hence contradiction; end; theorem [:X1,X2,X3,X4,X5,X6,X7,X8:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] implies X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5 & X6 meets Y6 & X7 meets Y7 &X8 meets Y8 proof A1: [:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:] = [:X1,X2,X3,X4,X5,X6,X7,X8:] & [:[:[:[:[:[:[:Y1,Y2:],Y3:],Y4:],Y5:],Y6:],Y7:],Y8:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] by Th12; A2: [:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:] = [:X1,X2,X3,X4,X5,X6,X7:] & [:[:[:[:[:[:Y1,Y2:],Y3:],Y4:],Y5:],Y6:],Y7:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] by MCART_4:11; assume [:X1,X2,X3,X4,X5,X6,X7,X8:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:]; then [:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:] meets [:[:[:[:[:[:Y1,Y2:],Y3:],Y4:],Y5:],Y6:],Y7:] & X8 meets Y8 by A1,ZFMISC_1:127; hence thesis by A2,MCART_4:26; end; theorem [:{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8}:] = { [x1,x2,x3,x4,x5,x6,x7,x8] } proof thus [:{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8}:] = [:[:{x1},{x2}:],{x3},{x4},{x5},{x6},{x7},{x8}:] by Th18 .= [:{[x1,x2]}, {x3},{x4},{x5},{x6},{x7},{x8}:] by ZFMISC_1:35 .= { [[x1,x2], x3, x4, x5, x6, x7, x8]} by MCART_4:27 .= { [x1,x2,x3,x4,x5,x6,x7,x8] } by Th9; end; reserve A1 for Subset of X1, A2 for Subset of X2, A3 for Subset of X3, A4 for Subset of X4, A5 for Subset of X5, A6 for Subset of X6, A7 for Subset of X7, A8 for Subset of X8; :: 8 - Tuples reserve x for Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} implies for x1,x2,x3,x4,x5,x6,x7,x8 st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 & x`5 = x5 & x`6 = x6 & x`7 = x7 & x`8 = x8 by Def3,Def4,Def5,Def6,Def7,Def8,Def9, Def10; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & (for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y1 = xx1) implies y1 =x`1 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} and A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y1 = xx1; x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8] by A1,Th25; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & (for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y2 = xx2) implies y2 =x`2 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} and A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y2 = xx2; x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8] by A1,Th25; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & (for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y3 = xx3) implies y3 =x`3 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} and A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y3 = xx3; x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8] by A1,Th25; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & (for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y4 = xx4) implies y4 =x`4 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} and A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y4 = xx4; x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8] by A1,Th25; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & (for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y5 = xx5) implies y5 =x`5 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} and A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y5 = xx5; x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8] by A1,Th25; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & (for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y6 = xx6) implies y6 =x`6 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} and A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y6 = xx6; x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8] by A1,Th25; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & (for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y7 = xx7) implies y7 =x`7 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} and A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y7 = xx7; x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8] by A1,Th25; hence thesis by A2; end; theorem X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & (for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y8 = xx8) implies y8 =x`8 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} and A2: for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8 st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y8 = xx8; x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8] by A1,Th25; hence thesis by A2; end; theorem y in [: X1,X2,X3,X4,X5,X6,X7,X8 :] implies ex x1,x2,x3,x4,x5,x6,x7,x8 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 & y = [x1,x2,x3,x4,x5,x6,x7,x8] proof assume y in [: X1,X2,X3,X4,X5,X6,X7,X8 :]; then y in [:[:X1,X2,X3,X4,X5,X6,X7:],X8:] by Def2; then consider x1234567, x8 being set such that A1: x1234567 in [:X1,X2,X3,X4,X5,X6,X7:] and A2: x8 in X8 and A3: y = [x1234567,x8] by ZFMISC_1:def 2; consider x1, x2, x3, x4, x5, x6, x7 such that A4: x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x1234567 = [x1,x2,x3,x4,x5,x6,x7] by A1,MCART_4:36; y = [x1,x2,x3,x4,x5,x6,x7,x8] by A3,A4,Def1; hence thesis by A2,A4; end; theorem [x1,x2,x3,x4,x5,x6,x7,x8] in [: X1,X2,X3,X4,X5,X6,X7,X8 :] iff x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 proof A1: [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2:],X3,X4,X5,X6,X7,X8:] by Th18; A2: [x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2],x3,x4,x5,x6,x7,x8] by Th9; [x1,x2] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:106; hence thesis by A1,A2,MCART_4:37; end; theorem (for y holds y in Z iff ex x1,x2,x3,x4,x5,x6,x7,x8 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 & y = [x1,x2,x3,x4,x5,x6,x7,x8]) implies Z = [: X1,X2,X3,X4,X5,X6,X7,X8 :] proof assume A1: for y holds y in Z iff ex x1,x2,x3,x4,x5,x6,x7,x8 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 & y = [x1,x2,x3,x4,x5,x6,x7,x8]; now let y; thus y in Z implies y in [:[:X1,X2,X3,X4,X5,X6,X7:],X8:] proof assume y in Z; then consider x1,x2,x3,x4,x5,x6,x7,x8 such that A2: x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x8 in X8 & y = [x1,x2,x3,x4,x5,x6,x7,x8] by A1; A3: y = [[x1,x2,x3,x4,x5,x6,x7],x8] by A2,Def1; [x1,x2,x3,x4,x5,x6,x7] in [:X1,X2,X3,X4,X5,X6,X7:] & x8 in X8 by A2,MCART_4:37; hence y in [:[:X1,X2,X3,X4,X5,X6,X7:],X8:] by A3,ZFMISC_1:def 2; end; assume y in [:[:X1,X2,X3,X4,X5,X6,X7:],X8:]; then consider x1234567,x8 being set such that A4: x1234567 in [:X1,X2,X3,X4,X5,X6,X7:] and A5: x8 in X8 and A6: y = [x1234567,x8] by ZFMISC_1:def 2; consider x1,x2,x3,x4,x5,x6,x7 such that A7: x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5 & x6 in X6 & x7 in X7 & x1234567 = [x1,x2,x3,x4,x5,x6,x7] by A4,MCART_4:36; y = [x1,x2,x3,x4,x5,x6,x7,x8] by A6,A7,Def1; hence y in Z by A1,A5,A7; end; then Z = [:[:X1,X2,X3,X4,X5,X6,X7:],X8:] by TARSKI:2; hence Z = [: X1,X2,X3,X4,X5,X6,X7,X8 :] by Def2; end; theorem Th42: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} & Y5<>{} & Y6<>{} & Y7<>{} & Y8<>{} implies for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:], y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] holds x = y implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3 & x`4 = y`4 & x`5 = y`5 & x`6 = y`6 & x`7 = y`7 & x`8 = y`8 proof assume that A1: X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} and A2: Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} & Y5<>{} & Y6<>{} & Y7<>{} & Y8<>{}; let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]; let y be Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:]; assume A3: x = y; thus x`1 = (x qua set)`1`1`1`1`1`1`1 by A1,Th26 .= y`1 by A2,A3,Th26; thus x`2 = (x qua set)`1`1`1`1`1`1`2 by A1,Th26 .= y`2 by A2,A3,Th26; thus x`3 = (x qua set)`1`1`1`1`1`2 by A1,Th26 .= y`3 by A2,A3,Th26; thus x`4 = (x qua set)`1`1`1`1`2 by A1,Th26 .= y`4 by A2,A3,Th26; thus x`5 = (x qua set)`1`1`1`2 by A1,Th26 .= y`5 by A2,A3,Th26; thus x`6 = (x qua set)`1`1`2 by A1,Th26 .= y`6 by A2,A3,Th26; thus x`7 = (x qua set)`1`2 by A1,Th26 .= y`7 by A2,A3,Th26; thus x`8 = (x qua set)`2 by A1,Th26 .= y`8 by A2,A3,Th26; end; theorem for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] st x in [:A1,A2,A3,A4,A5,A6,A7,A8:] holds x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4 & x`5 in A5 & x`6 in A6 & x`7 in A7 & x`8 in A8 proof let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]; assume A1: x in [:A1,A2,A3,A4,A5,A6,A7,A8:]; then A2: A1<>{} & A2<>{} & A3<>{} & A4<>{} & A5<>{} & A6<>{} & A7<>{} & A8<> {} by Th19; reconsider y = x as Element of [:A1,A2,A3,A4,A5,A6,A7,A8:] by A1; y`1 in A1 & y`2 in A2 & y`3 in A3 & y`4 in A4 & y`5 in A5 & y`6 in A6 & y`7 in A7 & y`8 in A8 by A2; hence x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4 & x`5 in A5 & x`6 in A6 & x`7 in A7 & x`8 in A8 by Th42; end; theorem Th44: X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 & X6 c= Y6 & X7 c= Y7 & X8 c= Y8 implies [:X1,X2,X3,X4,X5,X6,X7,X8:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] proof assume X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 & X6 c= Y6 & X7 c= Y7; then A1: [:X1,X2,X3,X4,X5,X6,X7:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] by MCART_4:41 ; A2: [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3,X4,X5,X6,X7:],X8:] & [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] = [:[:Y1,Y2,Y3,Y4,Y5,Y6,Y7:],Y8:] by Def2; assume X8 c= Y8; hence thesis by A1,A2,ZFMISC_1:119; end; theorem [:A1,A2,A3,A4,A5,A6,A7,A8:] is Subset of [:X1,X2,X3,X4,X5,X6,X7,X8:] by Th44 ;

Back to top