theorem :: MCART_1:39
for x1, x2, x3, y1, y2 being object holds [:{x1,y1},{x2,y2},{x3}:] = {[x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3]}