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