theorem :: MCART_1:9

for X being set st X <> {} holds
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] ) ) )