theorem :: MCART_1:61

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