:: deftheorem defines All ZF_LANG:def 24 :
for x, y being Variable
for H being ZF-formula holds All (x,y,H) = All (x,(All (y,H)));