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