for p being ZF-formula
for x being Variable holds
( bound_in (All (x,p)) = x & the_scope_of (All (x,p)) = p )