theorem Th37: :: MCART_1:49

for X1, X2, X3, X4 being set holds [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:]