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