The continuous dual separates points in a Hausdorff locally convex space

Fix $x\mathrm{\ne }y$ and put $v=x-y\mathrm{\ne }0$. Hausdorffness gives an open neighborhood $U$ of zero not containing $v$, by taking disjoint open neighborhoods of zero and $v$. Refine $U$ to an open convex zero-neighborhood $V\subseteq U$. The singleton $\{v\}$ is convex and nonempty, and misses $V$.

Apply open separation to $V$ and $\{v\}$. There are $f\in X^{\mathrm{\prime }}$ and $\alpha \in \mathbb{R}$ with $0=\mathrm{Re}f(0)<\alpha \le \mathrm{Re}f(v)$. Consequently $\mathrm{Re}f(x)-\mathrm{Re}f(y)=\mathrm{Re}f(v)>0$. The only non-ZF input is the HB application inside that separation theorem.

Every linear functional vanishes at zero, so zero belongs to the intersection of the kernels. For nonzero $v$, step 2.1 applied to $x=v,y=0$ gives a functional with nonzero real part at $v$, hence $v$ does not belong to that intersection. This proves the kernel identity from point separation.

Conversely, assume the kernel identity and fix $x\mathrm{\ne }y$, with $v=x-y$. Some $f\in X^{\mathrm{\prime }}$ has $z=f(v)\mathrm{\ne }0$. Over $\mathbb{R}$ this already separates real parts. Over $\mathbb{C}$, if $\mathrm{Re}z\mathrm{\ne }0$ again use $f$; otherwise $\mathrm{Im}z\mathrm{\ne }0$, and $g=-if\in X^{\mathrm{\prime }}$ has $\mathrm{Re}g(v)=\mathrm{Im}z\mathrm{\ne }0$. Thus the kernel identity implies the stated real-part separation. For $X=\{0\}$ there are no distinct points, and the kernel identity still holds. The proof selects a functional only for one fixed pair, never a simultaneous family.