Valuative criterion for properness

Work with the notions of valuative diagram and lift from [F2]. Assume first that $f$ is proper. Then [F1] makes $f$ separated, of finite type and universally closed, and [F5] makes it quasi-compact. Since $f$ is quasi-compact, the existence half of [F3] gives, for every valuative diagram for $f$ over every valuation ring, at least one lift. Since $f$ is separated and quasi-separated, the forward half of [F4] gives that every such diagram has at most one lift. Hence every valuative diagram has exactly one lift.

Assume conversely that every valuative diagram for $f$ over an arbitrary valuation ring has exactly one lift. The hypotheses give that $f$ is of finite type and quasi-separated, so [F5] makes $f$ quasi-compact. Existence of lifts for every diagram, together with quasi-compactness, gives that $f$ is universally closed by the reverse half of [F3]. Uniqueness of lifts, together with quasi-separatedness, gives that $f$ is separated by the reverse half of [F4]. Being separated, of finite type and universally closed, $f$ is proper by [F1].

The argument uses the Axiom of Choice exactly through the two cited criteria [F3] and [F4], each of which assumes it; no further choice is made here. Quasi-separatedness is used only in the uniqueness halves, and it is a separate hypothesis: [F6] defines it by quasi-compactness of intersections of affine opens over a common affine base open, whereas finite type contributes quasi-compactness by [F5]. If $X$ is empty, there is no morphism from the nonempty scheme $\mathrm{Spec}K$ to $X$, so there are no valuative diagrams and both lift conditions hold vacuously. If $S$ is empty, the only morphism $X\to S$ has $X$ empty, and the same reasoning applies. The statement has no endpoint cases.