[step:Separate the face from the remaining vertices modulo its affine hull]Define $\operatorname{aff}(F)$ to be the affine hull of $F$, namely the smallest affine subspace of $\mathbb{R}^n$ containing $F$. Define $\operatorname{relint}(F)$ to be the interior of $F$ with respect to the [subspace topology](/page/Subspace%20Topology) on $\operatorname{aff}(F)$.
Since $F$ is non-empty and, by the preceding step, is the convex hull of finitely many points, its relative interior in $\operatorname{aff}(F)$ is non-empty. Choose a point $x_0 \in \operatorname{relint}(F)$. Let
\begin{align*}
L := \operatorname{span}\{x-x_0 : x\in F\}
\end{align*}
be the direction space of the affine hull of $F$, and let
\begin{align*}
q:\mathbb{R}^n \to \mathbb{R}^n/L
\end{align*}
be the quotient map. Since $\operatorname{aff}(F)=x_0+L$, every point of $F$ has quotient $q(x_0)$.
We record the needed intersection property:
\begin{align*}
P\cap \operatorname{aff}(F)=F.
\end{align*}
The inclusion $F\subset P\cap \operatorname{aff}(F)$ follows from $F\subset P$ and the definition of $\operatorname{aff}(F)$. Conversely, let $z\in P\cap \operatorname{aff}(F)$. Since $x_0\in \operatorname{relint}(F)$ and $z\in \operatorname{aff}(F)$, there exists $\varepsilon>0$ such that
\begin{align*}
y:=x_0+\varepsilon(x_0-z)\in F.
\end{align*}
Then $y\in P$, and
\begin{align*}
x_0=\frac{1}{1+\varepsilon}y+\frac{\varepsilon}{1+\varepsilon}z
\end{align*}
is a convex combination of two points of $P$ with coefficients in $(0,1)$. Since $x_0\in F$ and $F$ is a face of $P$, the face property implies $z\in F$. Thus $P\cap \operatorname{aff}(F)=F$.
Let
\begin{align*}
J := \{1,\dots,m\}\setminus I.
\end{align*}
Since $F$ is proper and $P=\operatorname{conv}\{v_1,\dots,v_m\}$, the set $J$ is non-empty. Define
\begin{align*}
K := \operatorname{conv}\{q(v_j) : j\in J\} \subset \mathbb{R}^n/L.
\end{align*}
We have $q(x_0)\notin K$. Indeed, if $q(x_0)\in K$, then there exist $\mu_j\in[0,1]$ for $j\in J$ with
\begin{align*}
\sum_{j\in J}\mu_j = 1,
\qquad
q(x_0)=\sum_{j\in J}\mu_j q(v_j).
\end{align*}
Define
\begin{align*}
z := \sum_{j\in J}\mu_j v_j \in P.
\end{align*}
Then $q(z)=q(x_0)$, so $z-x_0\in L$. Hence $z\in x_0+L=\operatorname{aff}(F)$. Since $z\in P\cap \operatorname{aff}(F)$, the intersection property just proved gives $z\in F$. But $z$ is a convex combination only of vertices $v_j$ with $j\in J$, and the face property from the preceding step forces every vertex with positive coefficient into $F$, contradicting $j\in J$.
Therefore $q(x_0)$ and the compact convex set $K$ are disjoint in the finite-dimensional [vector space](/page/Vector%20Space) $\mathbb{R}^n/L$. By finite-dimensional strict separation, there exists a linear functional
\begin{align*}
\varphi:\mathbb{R}^n/L \to \mathbb{R}
\end{align*}
such that
\begin{align*}
\varphi(q(x_0)) > \varphi(y)
\end{align*}
for every $y\in K$.[/step]