theorem Th8: :: ZF_LANG1:8

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