theorem Th25: :: MCART_1:35

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