theorem Th19: :: MCART_1:26
for X being set st X <> {} holds
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] ) ) )