Membership in $\mathrm{PlaneCurveZeroSet}\,p$ holds exactly when $p$ evaluates to zero at $x$

Let $p$ be a bivariate real polynomial in $\mathrm{MvPolynomial}\,(\mathrm{Fin}\,2)\,\mathbb{R}$ and $x$ a point of the Euclidean plane $\mathrm{Point2}$. Then membership $x \in \mathrm{PlaneCurveZeroSet}\,p$ holds exactly when the evaluation vanishes,

and the two conditions coincide by definitional unfolding (Iff.rfl): $\mathrm{PlaneCurveZeroSet}\,p$ is defined as the set of points at which $p$ evaluates to zero.

This is the basic membership unfolding lemma for plane curves: it converts the geometric statement "$x$ lies on the curve cut out by $p$" into the algebraic equation $p(x) = 0$. It is used throughout the preliminaries whenever a set-theoretic fact about zero sets must be reduced to polynomial arithmetic.