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