theorem :: MCART_1:15

for x1, x2, z being object
for Y being set st z in [:{x1,x2},Y:] holds
( ( z `1 = x1 or z `1 = x2 ) & z `2 in Y )