theorem :: MCART_1:41

for x1, x2, x3, y2, y3 being object holds [:{x1},{x2,y2},{x3,y3}:] = {[x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]}