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

( 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