theorem Th9: :: ZF_LANG1:9

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