theorem :: ZF_LANG1:37

for H being ZF-formula st H is existential holds
( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative )