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