Problem on Hahn-Banach and separation theorem A problem on Hahn-Banach theorem and convex separation theorem:

Let $X$ be a real normed linear space. $E$ a convex subset of $X$ with nonempty interior, $F$ a linear subspace, with $(\operatorname{Int} E)\cap F=\emptyset$. Then there exists a bounded linear functional $f\in X^*, f\not\equiv0$, such that $f(E)\leq0,f(F)=0$.

I think the following corollary of Hahn-Banach theorem may be somewhat useful, but I can't figure out how to combine it with the convex separation theorem.

Let $A$ be a linear subspace of normed linear space $X$, $x_0\in X$, $d(x_0,A)>0$, then there exists $f\in X^*$ s.t. $f(A)=0,f(x_0)=d(x_0,A)$ and $||f||=1$.

Thanks for any help or suggestions.
 A: The statement you want to prove is the classic first version of the Hahn-Banach Separation Theorem .
Usually one has available the Hahn-Banach Theorem, in the form

If $M\subset X$ is a subspace, $\varphi:M\to\mathbb R$ is linear, and $\mu$ is a real seminorm on $X$ (subadditive, $\mu(\lambda x)=\lambda\,\mu(x)$ for $\lambda\geq0$) with $|\varphi(x)|\leq\mu(x)$ for all $x\in M$, then there exists $\tilde\varphi:X\to\mathbb R$, linear, with $\tilde\varphi|_M=\varphi$ and $|\tilde\varphi(x)|\leq\mu(x)$ for all $x$.

Since the interior of a convex set is convex, we may assume that $E$ is open (as the inequality will hold for any limit point). Fix $e'\in E$, $f'\in F$; The condition $E\cap F=\varnothing$ guarantees $e'\ne f'$. Then the set $Z=E-F+f'-e'$ is convex, open and $0\in E-F+f'-e'$. If $\mu$ is its Minkowski Functional, the conditions on $Z$ (open convex neighbourhood of $0$) guarantee that
$$\tag1
Z=\{x\in X:\ \mu(x)<1\}. 
$$
On the subspace $M=\mathbb R(f'-e')$, define $\varphi:M\to\mathbb R$ by $\varphi(\lambda(f'-e'))=\lambda$. Then $\varphi$ is linear. As $f'-e'\not\in Z$, we have $\mu(f'-e')\geq1$. So
$$
|\varphi(\lambda(f'-e'))|=|\lambda|\leq|\lambda|\,\mu(f'-e')=\mu(\lambda(f'-e')).
$$
That is, $|\varphi(x)|\leq\mu(x)$ for all $x\in M$. By the Hahn-Banach Theorem, there exists $\tilde\varphi:X\to\mathbb R$, linear, with $|\tilde\varphi(x)|\leq\mu(x)$ for all $x\in X$.
Now, for any $e\in E$, $f\in F$,
$$
\tilde\varphi(e)-\tilde\varphi(f)+1=\tilde\varphi(e-f+f'-e)<1
$$
by $(1)$. Thus
$$\tag2
\tilde\varphi(e)<\tilde\varphi(f),\qquad e\in E,\ f\in F. 
$$
Let $c=\sup\{\tilde\varphi(e):\ e\in E\}$. Then $c\leq\tilde\varphi(f)$ for all $f\in F$. Using that $F$ is a subspace, we get $c\leq t\tilde\varphi(f)$ for all $t\in\mathbb R$. This forces $\tilde\varphi(f)=0$ for all $f\in F$. Thus
$$\tag3
\tilde\varphi(f)=0,\ \tilde\varphi(e)\leq0,\qquad f\in F,\ e\in E. 
$$
Finally,  limit points of $E$ are also limit points of $Z$, and so they satisfy $\mu(x)\leq1$ as the Minkowski Functional is continuous. So the argument above still works, just with $\leq$ instead of $<$.
