let x be Variable; for H being ZF-formula holds
( the_scope_of (All (x,H)) = H & bound_in (All (x,H)) = x )
let H be ZF-formula; ( 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; verum