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 Th43;
hence H = Ex ((bound_in H),(the_scope_of H)) by A1, Th43; :: thesis: verum