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