theorem :: MCART_1:16

for y1, y2, z being object
for X being set st z in [:X,{y1,y2}:] holds
( z `1 in X & ( z `2 = y1 or z `2 = y2 ) )