theorem Th38: :: MCART_1:50

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