:: deftheorem defines existential ZF_LANG:def 23 :
for H being ZF-formula holds
( H is existential iff ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) );