let X be set ; :: thesis: ( X <> {} implies ex v being object st
( v in X & ( for x, y, z being object holds
( ( not x in X & not y in X ) or not v = [x,y,z] ) ) ) )
assume X <> {} ; :: thesis: ex v being object st
( v in X & ( for x, y, z being object 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 XREGULAR:4;
take v = Y; :: thesis: ( v in X & ( for x, y, z being object 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 object holds
( ( not x in X & not y in X ) or not v = [x,y,z] )
given x, y, z being object 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};
A5: ( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
A6: {{{x,y},{x}},z} in Y by A4, TARSKI:def 2;
( {x,y} in {{x,y},{x}} & {{x,y},{x}} in {{{x,y},{x}},z} ) by TARSKI:def 2;
hence contradiction by A2, A5, A6, A3, XBOOLE_0:3; :: thesis: verum