thus ex a, A being set st
( ( for x, y being Variable holds
( [(x '=' y),H₇(x,y)] in A & [(x 'in' y),H₈(x,y)] in A ) ) & [H,a] in A & ( for H' being ZF-formula
for a being set st [H',a] in A holds
( ( H' is being_equality implies a = H₇( Var1 H', Var2 H') ) & ( H' is being_membership implies a = H₈( Var1 H', Var2 H') ) & ( H' is negative implies ex b being set st
( a = H₉(b) & [(the_argument_of H'),b] in A ) ) & ( H' is conjunctive implies ex b, c being set st
( a = H₁₀(b,c) & [(the_left_argument_of H'),b] in A & [(the_right_argument_of H'),c] in A ) ) & ( H' is universal implies ex b being set st
( a = H₁₁( bound_in H',b) & [(the_scope_of H'),b] in A ) ) ) ) ) from ZF_MODEL:sch 1(); :: thesis: verum