let X be set ; ( X <> {} implies ex v being object st
( v in X & ( for x1, x2, x3, x4 being object holds
( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] ) ) ) )
assume
X <> {}
; ex v being object st
( v in X & ( for x1, x2, x3, x4 being object holds
( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] ) ) )
then consider Y being set such that
A1:
Y in X
and
A2:
for Y1, Y2, Y3, Y4, Y5 being set st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y holds
Y1 misses X
by XREGULAR:6;
take v = Y; ( v in X & ( for x1, x2, x3, x4 being object holds
( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] ) ) )
thus
v in X
by A1; for x1, x2, x3, x4 being object holds
( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] )
given x1, x2, x3, x4 being object such that A3:
( x1 in X or x2 in X )
and
A4:
v = [x1,x2,x3,x4]
; 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};
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;
A6:
{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4} in Y
by A4, TARSKI:def 2;
A7:
( x1 in {x1,x2} & x2 in {x1,x2} )
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, A7, A5, A6, A3, XBOOLE_0:3; verum