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