= Solution
Let $D\in M$ be a <dense subset of a forcing order> $\mathbb P$. Then $D\times\mathbb Q\in M$ is dense in the <product forcing> order: below $(p,q)$, choose $p'\leq p$ in $D$ and retain $q$. The <generic filter> $H$ meets it, so its first projection $G_0$ meets $D$. Together with the filter properties proved above, this gives
$$
\boxed{G_0\text{ is }\mathbb P\text{-generic over }M.}
$$
The same argument proves that $G_1$ is $\mathbb Q$-generic over $M$, but genericity over the larger <generic extension> $M[G_0]$ needs the next argument.
Back to article page
