# Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Corollary 5.1.3.9. Let $q: X \rightarrow S$ be an inner fibration of simplicial sets, let $z$ be a vertex of $X$, and let $e: s \rightarrow q(z)$ be an edge of $S$. Suppose that there exists a $q$-cartesian edge $g: y \rightarrow z$ of $X$ satisfying $q(g) = e$. Then any locally $q$-cartesian edge $h: x \rightarrow z$ satisfying $q(h) = e$ is $q$-cartesian.

Proof. By virtue of Remark 5.1.1.12, we may assume without loss of generality that $S$ is an $\infty$-category (or even a simplex). Applying Remark 5.1.3.8, we deduce that there is a $2$-simplex of $X$ as depicted in the diagram

$\xymatrix@R =50pt@C=50pt{ & y \ar [dr]^{g} & \\ x \ar [ur]^{f} \ar [rr]^-{h} & & z, }$

where $f$ is an isomorphism in the $\infty$-category $X$. Then $f$ is also $q$-cartesian (Proposition 5.1.1.8), so Corollary 5.1.2.4 guarantees that $h$ is $q$-cartesian. $\square$