let x be Variable; :: thesis: for H, H1 being ZF-formula st H is existential holds
( ( x = bound_in H implies ex H1 being ZF-formula st Ex x,H1 = H ) & ( ex H1 being ZF-formula st Ex x,H1 = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex x,H1 = H ) & ( ex x being Variable st Ex x,H1 = H implies H1 = the_scope_of H ) )
let H, H1 be ZF-formula; :: thesis: ( H is existential implies ( ( x = bound_in H implies ex H1 being ZF-formula st Ex x,H1 = H ) & ( ex H1 being ZF-formula st Ex x,H1 = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex x,H1 = H ) & ( ex x being Variable st Ex x,H1 = H implies H1 = the_scope_of H ) ) )
assume A1: H is existential ; :: thesis: ( ( x = bound_in H implies ex H1 being ZF-formula st Ex x,H1 = H ) & ( ex H1 being ZF-formula st Ex x,H1 = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex x,H1 = H ) & ( ex x being Variable st Ex x,H1 = H implies H1 = the_scope_of H ) )
then consider y being Variable, F being ZF-formula such that
A2: H = Ex y,F by Def23;
H . 1 = 2 by A2, FINSEQ_1:58;
then not H is universal by Th39;
hence ( ( x = bound_in H implies ex H1 being ZF-formula st Ex x,H1 = H ) & ( ex H1 being ZF-formula st Ex x,H1 = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex x,H1 = H ) & ( ex x being Variable st Ex x,H1 = H implies H1 = the_scope_of H ) ) by A1, Def33, Def34; :: thesis: verum