theorem Th20: :: MCART_1:30

for X being set st X <> {} holds
ex v being object st
( v in X & ( for x1, x2, x3, x4 being object holds
( ( not x1 in X & not x2 in X ) or not v = [x1,x2,x3,x4] ) ) )