Equations vanishing on the infinitely many real points of an irreducible $P$ cut out exactly the curve $P=0$

Let $P\in\mathbb C[X,Y]$ be irreducible. Writing points of the real plane as $z\in\mathbb C$, the real locus of $P$ in the coordinates $X=z$, $Y=\bar z$ is $Z(P)=\{z\in\mathbb C:P(z,\bar z)=0\}$. Let $\Delta_P=\{(z,\bar z):z\in Z(P)\}\subseteq\mathbb C^2$ be its image under $z\mapsto(z,\bar z)$, and let $I(\Delta_P)=\{Q\in\mathbb C[X,Y]:Q(v)=0\ \text{for all}\ v\in\Delta_P\}$ be the ideal of the polynomials vanishing on $\Delta_P$.

If $Z(P)$ is infinite, then

In the classical Zariski topology of $\mathbb C^2$ this says that the closure of the real points $\Delta_P$ is the whole complex curve $P=0$: the Zariski density of an infinite real locus that the note invokes in the proofs of Lemma 3 and Theorem 2. For the polynomial $P_\alpha$ of equation (6), with $|\alpha|=1$ and $\alpha\notin\mathbb R$ as in Lemma 4, the points $(z,\bar z)$ with $z\in C_{m,\alpha}$ are therefore Zariski dense in the complex affine curve $P_\alpha=0$, the affine part of the curve $V_\alpha\subset\mathbb P^1\times\mathbb P^1$ obtained by closing (6).

Formalization Note: the left side is Mathlib's MvPolynomial.zeroLocus ℂ of MvPolynomial.vanishingIdeal ℂ, with irreducibility taken in MvPolynomial (Fin 2) ℂ.