Separation of a point from a closed linear subspace ($f(x_0)=1,f{|}_Y=0$)

If $Y$ is a closed linear subspace of a Hausdorff locally convex space and $x_0\notin Y$, choose a continuous seminorm $q$ with $q(x_0-y)\ge 1$ for all $y\in Y$, using a basic neighborhood disjoint from $Y$. The linear functional $g(y+t{x}_0)=t$ is bounded by $q$. The Hahn-Banach theorem extends it to a continuous linear functional with the displayed values. This is the linear-subspace form of separation, sharper than merely distinguishing the two sets.