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 ex y being Variable ex F being ZF-formula st H = Ex (y,F) ;
then H . 1 = 2 by FINSEQ_1:41;
then not H is universal by Th22;
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