Corollary 5.1.1.15. Let $q: X \rightarrow S$ and $f: K \rightarrow X$ be morphisms of simplicial sets, and let $q': X_{f/} \rightarrow S_{ (q \circ f)/ }$ be the morphism induced by $q$. Let $\overline{e}: \overline{x} \rightarrow \overline{y}$ be an edge of the simplicial set $X_{f/}$, and let $e: x \rightarrow y$ be its image in $X$. If $e$ is $q$-cartesian, then $\overline{e}$ is $q'$-cartesian.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. Since $e$ is $q$-cartesian, the restriction map
\[ \theta : X_{/e} \rightarrow X_{/y} \times _{ S_{/q(y)} } S_{/q(e)} \]
is a trivial Kan fibration (Proposition 5.1.1.14). We wish to show that the restriction map
\[ \overline{\theta }: (X_{f/} )_{ / \overline{e} } \rightarrow (X_{f/} )_{ / \overline{y} } \times _{ (S_{(q \circ f)/} )_{ / q'( \overline{y} )}} (S_{ (q \circ f)/} )_{ / q'( \overline{e} ) }. \]
is also a trivial Kan fibration. We can identify $\overline{e}$ with a morphism of simplicial sets $\overline{f}: K \rightarrow X_{/e}$, and $\overline{\theta }$ with the induced map
\[ ( X_{/e} )_{\overline{f} / } \rightarrow (X_{/y} \times _{ S_{/q(y)} } S_{/q(e)})_{ (\theta \circ \overline{f}) / }. \]
The desired result now follows from Corollary 4.3.7.17. $\square$