let X1, X2, X3, X4 be set ; :: thesis: [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:]
thus [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4
.= [:[:[:X1,X2:],X3:],X4:] by ZFMISC_1:def 3 ; :: thesis: verum