theorem :: MCART_1:14

for x, y, z being object st z in [:{x},{y}:] holds
( z `1 = x & z `2 = y )