let X be set ; :: thesis: ( X <> {} implies ex x being set st
( x in X & ( for x1, x2, x3, x4, x5 being set holds
( ( not x1 in X & not x2 in X ) or not x = [x1,x2,x3,x4,x5] ) ) ) )
assume X <> {} ; :: thesis: ex x being set st
( x in X & ( for x1, x2, x3, x4, x5 being set holds
( ( not x1 in X & not x2 in X ) or not x = [x1,x2,x3,x4,x5] ) ) )
then consider Y being set such that
A1: Y in X and
A2: for 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 Y holds
Y1 misses X by Th2;
take x = Y; :: thesis: ( x in X & ( for x1, x2, x3, x4, x5 being set holds
( ( not x1 in X & not x2 in X ) or not x = [x1,x2,x3,x4,x5] ) ) )
thus x in X by A1; :: thesis: for x1, x2, x3, x4, x5 being set holds
( ( not x1 in X & not x2 in X ) or not x = [x1,x2,x3,x4,x5] )
given x1, x2, x3, x4, x5 being set such that A3: ( x1 in X or x2 in X ) and
A4: x = [x1,x2,x3,x4,x5] ; :: thesis: 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};
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] by A4, Th3
.= [[[{{x1,x2},{x1}},x3],x4],x5] by TARSKI:def 5
.= [[{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4],x5] by TARSKI:def 5
.= [{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5] 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}}}}}}}} by TARSKI:def 5 ;
then A6: {{{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}},x4},{{{{{x1,x2},{x1}},x3},{{{x1,x2},{x1}}}}}},x5} 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;
( x1 in {x1,x2} & x2 in {x1,x2} ) by TARSKI:def 2;
then A8: not {x1,x2} misses X by A3, XBOOLE_0:3;
( {x1,x2} in {{x1,x2},{x1}} & {{x1,x2},{x1}} in {{{x1,x2},{x1}},x3} ) by TARSKI:def 2;
hence contradiction by A2, A8, A5, A7, A6; :: thesis: verum