:: deftheorem defines [: ZFMISC_1:def 4 :
for X1, X2, X3, X4 being set holds [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:];