theorem Th4: :: MCART_1:10

for z being object
for X, Y being set st z in [:X,Y:] holds
( z `1 in X & z `2 in Y )