Solution (source code)

= Solution

For the <product forcing> order, let $G_0$ and $G_1$ be the coordinate projections of $H$:
$$
G_0=\{p:\exists q\ ((p,q)\in H)\},\qquad G_1=\{q:\exists p\ ((p,q)\in H)\}.
$$
These are nonempty upward-closed, directed <filters in an ordered set>. Clearly $H\subseteq G_0\times G_1$. If $p\in G_0$ and $q\in G_1$, choose $(p,q')\in H$ and $(p',q)\in H$. Directedness supplies $(r,s)\in H$ below both, so $(r,s)\leq(p,q)$. Upward closure of $H$ gives $(p,q)\in H$. Therefore the <projection of a product-generic filter> satisfies
$$
\boxed{H=G_0\times G_1.}
$$
No greatest conditions in the factors are required for this argument.