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