let x be Variable; :: thesis: for H being ZF-formula holds
( the_scope_of (All x,H) = H & bound_in (All x,H) = x )
let H be ZF-formula; :: thesis: ( the_scope_of (All x,H) = H & bound_in (All x,H) = x )
All x,H is universal by ZF_LANG:16;
then All x,H = All (bound_in (All x,H)),(the_scope_of (All x,H)) by ZF_LANG:62;
hence ( the_scope_of (All x,H) = H & bound_in (All x,H) = x ) by ZF_LANG:12; :: thesis: verum