For each , choose a maximal antichain in a forcing order below deciding a witness in . Write the decided values as , one for each condition in that antichain. The -chain condition for forcing gives fewer than possible values. Since is regular in , choose
The possible-values lemma for chain-condition forcing ensures
In take the club set of limit closure points
It is unbounded by repeatedly closing any starting ordinal under for countably many steps, and closed by taking increasing limits. For , the forced displayed property gives points of arbitrarily high below . Its forced closedness yields . Therefore
This proves the ground-model club containment lemma. The name on the right is , as printed in the PDF.