let X be set ; ( X <> {} implies ex y being set st
( y in X & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set holds
( ( not x1 in X & not x2 in X ) or not y = [x1,x2,x3,x4,x5,x6,x7,x8] ) ) ) )
assume
X <> {}
; ex y being set st
( y in X & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set holds
( ( not x1 in X & not x2 in X ) or not y = [x1,x2,x3,x4,x5,x6,x7,x8] ) ) )
then consider Y being set such that
A1:
Y in X
and
A2:
for 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 Y holds
Y1 misses X
by Th117;
take y = Y; ( y in X & ( for x1, x2, x3, x4, x5, x6, x7, x8 being set holds
( ( not x1 in X & not x2 in X ) or not y = [x1,x2,x3,x4,x5,x6,x7,x8] ) ) )
thus
y in X
by A1; for x1, x2, x3, x4, x5, x6, x7, x8 being set holds
( ( not x1 in X & not x2 in X ) or not y = [x1,x2,x3,x4,x5,x6,x7,x8] )
given x1, x2, x3, x4, x5, x6, x7, x8 being set such that A3:
( x1 in X or x2 in X )
and
A4:
y = [x1,x2,x3,x4,x5,x6,x7,x8]
; contradiction
set Y1 = {x1,x2};
set Y2 = {{x1,x2},{x1}};
set Y3 = {{{x1,x2},{x1}},x3};
set Y4 = {{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}};
set Y5 = {{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4};
set Y6 = {{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}};
set Y7 = {{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5};
set Y8 = {{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}};
set Y9 = {{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6};
set YA = {{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}};
set YB = {{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7};
set YC = {{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7},{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}}}};
set YD = {{{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7},{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}}}},x8};
A5:
( {{{x1,x2},{x1}},x3} in {{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}} & {{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}} in {{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4} )
by TARSKI:def 2;
Y =
[[[[[[[x1,x2],x3],x4],x5],x6],x7],x8]
by A4, Th3
.=
[[[[[[{{x1,x2},{x1}},x3],x4],x5],x6],x7],x8]
by TARSKI:def 5
.=
[[[[[{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4],x5],x6],x7],x8]
by TARSKI:def 5
.=
[[[[{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5],x6],x7],x8]
by TARSKI:def 5
.=
[[[{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6],x7],x8]
by TARSKI:def 5
.=
[[{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7],x8]
by TARSKI:def 5
.=
[{{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7},{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}}}},x8]
by TARSKI:def 5
.=
{{{{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7},{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}}}},x8},{{{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7},{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}}}}}}
by TARSKI:def 5
;
then A6:
{{{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7},{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}}}},x8} in Y
by TARSKI:def 2;
A7:
( {{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4} in {{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}} & {{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}} in {{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5} )
by TARSKI:def 2;
A8:
( {{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7} in {{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7},{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}}}} & {{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7},{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}}}} in {{{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7},{{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}}}},x8} )
by TARSKI:def 2;
A9:
( {{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6} in {{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}} & {{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}} in {{{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6},{{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}}}},x7} )
by TARSKI:def 2;
( x1 in {x1,x2} & x2 in {x1,x2} )
by TARSKI:def 2;
then A10:
not {x1,x2} misses X
by A3, XBOOLE_0:3;
A11:
( {{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5} in {{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}} & {{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}} in {{{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5},{{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}}}},x6} )
by TARSKI:def 2;
( {x1,x2} in {{x1,x2},{x1}} & {{x1,x2},{x1}} in {{{x1,x2},{x1}},x3} )
by TARSKI:def 2;
hence
contradiction
by A2, A10, A5, A7, A11, A9, A8, A6; verum