theorem :: MCART_1:19

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