let H be ZF-formula; :: thesis: ( H is universal implies H = All (bound_in H),(the_scope_of H) )
assume A1: H is universal ; :: thesis: H = All (bound_in H),(the_scope_of H)
then ex x being Variable st H = All x,(the_scope_of H) by Def34;
hence H = All (bound_in H),(the_scope_of H) by A1, Def33; :: thesis: verum