:: deftheorem Def34 defines the_scope_of ZF_LANG:def 34 :
for H being ZF-formula st ( H is universal or H is existential ) holds
for b₂ being ZF-formula holds
( ( H is universal implies ( b₂ = the_scope_of H iff ex x being Variable st All (x,b₂) = H ) ) & ( not H is universal implies ( b₂ = the_scope_of H iff ex x being Variable st Ex (x,b₂) = H ) ) );