 One then shows that any generalized positive formula \(\phi(x)\) has an extension \(\{x \mid \phi(x)\}\) by considering the sets of witnesses to \(\phi(x)\) in each type \(n\); these sets themselves can be used to construct a convergent sequence (with the proviso that some apparent elements found at any given stage may need to be discarded; one defines \(s_{n+1}\) as the set of those type \(n\) approximants which not only witness \(\phi(x)\) at the current type \(n\) but have refinements which witness \(\phi(x)\) at each subsequent type. The sequence of sets \(s\) obtained will be an element of the intended model and have the intended extension.