[proofplan]
Write the polytope as the convex hull of finitely many vertices. First we prove that a face is exactly the convex hull of the vertices of $P$ that it contains. Then we separate this convex hull from the convex hull of the remaining vertices after quotienting by the affine hull of the face, so the separating functional is constant on the face and strictly smaller on every vertex outside it. Since a linear functional attains its maximum over a finite convex hull at the vertices, the resulting supporting hyperplane exposes precisely $F$.
[/proofplan]
[step:Write the face as the convex hull of the vertices it contains]
Since $P$ is a polytope, choose points $v_1,\dots,v_m \in \mathbb{R}^n$ such that
\begin{align*}
P = \operatorname{conv}\{v_1,\dots,v_m\}.
\end{align*}
Define the index set of vertices lying in the face by
\begin{align*}
I := \{i \in \{1,\dots,m\} : v_i \in F\}.
\end{align*}
We claim that
\begin{align*}
F = \operatorname{conv}\{v_i : i \in I\}.
\end{align*}
The inclusion $\operatorname{conv}\{v_i : i \in I\} \subset F$ follows because $F$ is convex. Conversely, let $x \in F$. Since $x \in P$, there exist coefficients $\lambda_1,\dots,\lambda_m \in [0,1]$ with
\begin{align*}
\sum_{i=1}^m \lambda_i = 1,
\qquad
x = \sum_{i=1}^m \lambda_i v_i.
\end{align*}
If $\lambda_j > 0$, then write
\begin{align*}
x = \lambda_j v_j + (1-\lambda_j)y_j,
\end{align*}
where, if $\lambda_j < 1$,
\begin{align*}
y_j := \frac{1}{1-\lambda_j}\sum_{i\neq j}\lambda_i v_i \in P,
\end{align*}
and if $\lambda_j = 1$, then $x = v_j$. In either case, the face property implies $v_j \in F$. Hence every index with $\lambda_j>0$ lies in $I$, and therefore
\begin{align*}
x = \sum_{i\in I}\lambda_i v_i \in \operatorname{conv}\{v_i : i\in I\}.
\end{align*}
[guided]
We first identify which vertices of $P$ belong to the face. Because $P$ is a polytope, it is the convex hull of finitely many points $v_1,\dots,v_m \in \mathbb{R}^n$:
\begin{align*}
P = \operatorname{conv}\{v_1,\dots,v_m\}.
\end{align*}
Define
\begin{align*}
I := \{i \in \{1,\dots,m\} : v_i \in F\}.
\end{align*}
We prove that $F$ is exactly the convex hull of those vertices:
\begin{align*}
F = \operatorname{conv}\{v_i : i \in I\}.
\end{align*}
The inclusion from right to left is immediate from convexity of $F$: every $v_i$ with $i\in I$ lies in $F$, and every convex combination of points of $F$ remains in $F$.
For the reverse inclusion, fix $x \in F$. Since $x \in P$, there are numbers $\lambda_1,\dots,\lambda_m \in [0,1]$ satisfying
\begin{align*}
\sum_{i=1}^m \lambda_i = 1,
\qquad
x = \sum_{i=1}^m \lambda_i v_i.
\end{align*}
We must show that no vertex outside $F$ can occur with positive coefficient. Suppose $\lambda_j>0$. If $\lambda_j<1$, define
\begin{align*}
y_j := \frac{1}{1-\lambda_j}\sum_{i\neq j}\lambda_i v_i.
\end{align*}
Then $y_j\in P$, because it is a convex combination of the points $v_i$, and
\begin{align*}
x = \lambda_j v_j + (1-\lambda_j)y_j.
\end{align*}
Since $x\in F$ and $F$ is a face of $P$, the defining face property forces both endpoints of this non-trivial convex decomposition to lie in $F$; in particular $v_j\in F$. If $\lambda_j=1$, then $x=v_j$, so again $v_j\in F$. Thus every vertex appearing with positive coefficient belongs to $F$, which means every such index belongs to $I$. Hence
\begin{align*}
x = \sum_{i\in I}\lambda_i v_i \in \operatorname{conv}\{v_i : i\in I\}.
\end{align*}
This proves $F=\operatorname{conv}\{v_i:i\in I\}$.
[/guided]
[/step]
[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$.
[guided]
The notation $\operatorname{aff}(F)$ means the affine hull of $F$, namely the smallest affine subspace of $\mathbb{R}^n$ containing $F$. The notation $\operatorname{relint}(F)$ means the interior of $F$ with respect to the subspace topology on $\operatorname{aff}(F)$.
The next goal is to build a linear functional that is constant on $F$. A linear functional is constant on $F$ exactly when it vanishes on all differences of points of $F$. We encode those differences by choosing a point in the relative interior of $F$. This is possible because the preceding step writes $F$ as the convex hull of finitely many points, so $F$ is a non-empty polytope inside its affine hull. Choose
\begin{align*}
x_0\in \operatorname{relint}(F).
\end{align*}
Define
\begin{align*}
L := \operatorname{span}\{x-x_0 : x\in F\}.
\end{align*}
This is the direction space of the affine hull of $F$, so $\operatorname{aff}(F)=x_0+L$. Let
\begin{align*}
q:\mathbb{R}^n \to \mathbb{R}^n/L
\end{align*}
be the quotient map. Every point of $F$ has the same image under $q$, namely $q(x_0)$.
We also need the fact that no point of $P$ outside $F$ lies in the affine hull of $F$. We prove
\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)$. For the reverse inclusion, take $z\in P\cap \operatorname{aff}(F)$. Because $x_0$ lies in the relative interior of $F$, moving a sufficiently small distance from $x_0$ in any direction inside $\operatorname{aff}(F)$ stays in $F$. Applying this to the direction $x_0-z\in L$, choose $\varepsilon>0$ such that
\begin{align*}
y:=x_0+\varepsilon(x_0-z)\in F.
\end{align*}
Then $y\in P$, and the identity
\begin{align*}
x_0=\frac{1}{1+\varepsilon}y+\frac{\varepsilon}{1+\varepsilon}z
\end{align*}
expresses $x_0$ as a convex combination of $y$ and $z$ with both coefficients strictly between $0$ and $1$. Since $x_0\in F$ and $F$ is a face of $P$, the defining face property forces $z\in F$. Hence $P\cap \operatorname{aff}(F)=F$.
Let
\begin{align*}
J := \{1,\dots,m\}\setminus I
\end{align*}
be the set of indices of vertices not in $F$. This set is non-empty because $F$ is a proper face of $P$ and $P$ is the convex hull of the listed vertices. Define the compact convex set
\begin{align*}
K := \operatorname{conv}\{q(v_j) : j\in J\} \subset \mathbb{R}^n/L.
\end{align*}
We claim that $q(x_0)\notin K$. Suppose instead that $q(x_0)\in K$. Then there are coefficients $\mu_j\in[0,1]$ for $j\in J$ such that
\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.
\end{align*}
Then $z\in P$, because it is a convex combination of vertices of $P$, and $q(z)=q(x_0)$, so $z-x_0\in L$. Therefore $z\in x_0+L=\operatorname{aff}(F)$.
Now $z\in P\cap\operatorname{aff}(F)$. By the intersection property proved above, $P\cap\operatorname{aff}(F)=F$, so $z\in F$. But $z$ was written as a convex combination of vertices $v_j$ with $j\in J$, none of which lies in $F$. Applying the same face argument from the first step, every vertex appearing with positive coefficient in a convex representation of a point of $F$ must itself belong to $F$. This contradicts $j\in J$ for any positive coefficient. Hence $q(x_0)\notin K$.
Since $\mathbb{R}^n/L$ is finite-dimensional, and since the singleton $\{q(x_0)\}$ and the compact convex set $K$ are disjoint, finite-dimensional strict separation gives 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$.
[/guided]
[/step]
[step:Lift the separating functional to expose the face]
Define the linear functional
\begin{align*}
\ell:\mathbb{R}^n \to \mathbb{R}
\end{align*}
by
\begin{align*}
\ell := \varphi\circ q,
\end{align*}
and define
\begin{align*}
\alpha := \ell(x_0).
\end{align*}
For every $x\in F$, we have $q(x)=q(x_0)$, hence
\begin{align*}
\ell(x)=\alpha.
\end{align*}
For every $j\in J$, we have $q(v_j)\in K$, and therefore
\begin{align*}
\ell(v_j)=\varphi(q(v_j))<\varphi(q(x_0))=\alpha.
\end{align*}
For every $i\in I$, since $v_i\in F$, we have
\begin{align*}
\ell(v_i)=\alpha.
\end{align*}
Let $x\in P$. Choose coefficients $\lambda_1,\dots,\lambda_m\in[0,1]$ with
\begin{align*}
\sum_{i=1}^m \lambda_i=1,
\qquad
x=\sum_{i=1}^m \lambda_i v_i.
\end{align*}
By linearity,
\begin{align*}
\ell(x)
=
\sum_{i=1}^m \lambda_i\ell(v_i)
\leq
\sum_{i=1}^m \lambda_i\alpha
=
\alpha.
\end{align*}
Thus $\ell$ is maximised over $P$ on a subset containing $F$.
If $\ell(x)=\alpha$, then the displayed inequality can be an equality only if $\lambda_j=0$ for every $j\in J$, because $\ell(v_j)<\alpha$ for all $j\in J$. Hence
\begin{align*}
x=\sum_{i\in I}\lambda_i v_i \in \operatorname{conv}\{v_i:i\in I\}=F.
\end{align*}
Therefore
\begin{align*}
F=\{x\in P:\ell(x)=\alpha\},
\end{align*}
with $\ell(x)\leq \alpha$ for all $x\in P$. Since $F$ is proper, some $v_j$ lies outside $F$, and $\ell(v_j)<\alpha$, so $\ell$ is non-zero. Thus $F$ is an exposed face of $P$.
[/step]