$\mathrm{swapPoint}$ is an involution on the plane

Let $z : \mathrm{Point2}$ be any point of the Euclidean plane, and let $\mathrm{swapPoint}$ be the coordinate-swap map $z \mapsto \mathrm{mkPoint2}\,(z\,1)\,(z\,0)$. Then swapping twice is the identity:

This identity is used only inside the two nonsingular-point lemmas: the $\partial_0$ case (nonsingular_point_has_infinite_zeroSet_of_partial0) is derived from the $\partial_1$ case by renaming the two variables of the polynomial with the swap and moving points with $\mathrm{swapPoint}$. The identity shows that $\mathrm{swapPoint}$ is injective and that it maps the zero set of the renamed polynomial onto the zero set of the original one. The pair-intersection analysis does not swap coordinates.