[000W] Lemma 5.2·b.

The externalization [000V] is a cartesian fibration.

Proof. Given an object $v\in \brk{C}\Sub{y}$ and a morphism $f:x\to y$ in $E$, we may define a cartesian lift $\InvImg{f}v\to\Sub{f} v$ by setting $\InvImg{f}v = v\circ f : x \to C\Sub{0}$.