let X be set ; :: thesis: ( X <> {} implies ex v being set st
( v in X & ( for x, y, z being set holds
( ( not x in X & not y in X ) or not v = [x,y,z] ) ) ) )
assume X <> {} ; :: thesis: ex v being set st
( v in X & ( for x, y, z being set holds
( ( not x in X & not y in X ) or not v = [x,y,z] ) ) )
then consider Y being set such that
A1: Y in X and
A2: for Y1, Y2, Y3 being set holds
( not Y1 in Y2 or not Y2 in Y3 or not Y3 in Y or Y1 misses X ) by Th4;
take v = Y; :: thesis: ( v in X & ( for x, y, z being set holds
( ( not x in X & not y in X ) or not v = [x,y,z] ) ) )
thus v in X by A1; :: thesis: for x, y, z being set holds
( ( not x in X & not y in X ) or not v = [x,y,z] )
given x, y, z being set such that A3: ( x in X or y in X ) and
A4: v = [x,y,z] ; :: thesis: contradiction
set Y1 = {x,y};
set Y2 = {{x,y},{x}};
set Y3 = {{{x,y},{x}},z};
( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
then A5: not {x,y} misses X by A3, XBOOLE_0:3;
Y = [{{x,y},{x}},z] by A4, TARSKI:def 5
.= {{{{x,y},{x}},z},{{{x,y},{x}}}} by TARSKI:def 5 ;
then ( {x,y} in {{x,y},{x}} & {{x,y},{x}} in {{{x,y},{x}},z} & {{{x,y},{x}},z} in Y ) by TARSKI:def 2;
hence contradiction by A2, A5; :: thesis: verum