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 ;
then All (x,H) = All ((bound_in (All (x,H))),(the_scope_of (All (x,H)))) by ZF_LANG:44;
hence ( the_scope_of (All (x,H)) = H & bound_in (All (x,H)) = x ) by ZF_LANG:3; :: thesis: verum