Support of a finite-type quasi-coherent sheaf is closed

Let $U=\mathrm{Spec}A$ be an affine open with $\mathcal{F}{\mathrm{\mid }}_U\cong \tilde{M}$ for a finitely generated $A$-module $M$; then $\mathrm{Supp}(\mathcal{F})\cap U=\mathrm{Supp}(\mathcal{F}{\mathrm{\mid }}_U)$ by [F1] equals $\{\mathfrak{p}:(\tilde{M}{)}_{\mathfrak{p}}\mathrm{\ne }0\}$, which by [F2] is $\{\mathfrak{p}:M_{\mathfrak{p}}\mathrm{\ne }0\}={\mathrm{Supp}}_A(M)$, and by [F3] this is $\{\mathfrak{p}:{\mathrm{Ann}}_A(M)\subseteq \mathfrak{p}\}=V({\mathrm{Ann}}_A(M))$, the zero set of an ideal and hence closed in $U=\mathrm{Spec}A$.

Let $\{U_i{\}}_{i\in I}$ be the family of all affine open subsets $U_i$ of $X$ with $\mathcal{F}{\mathrm{\mid }}_{U_i}\cong \widetilde{M_i}$ for a finitely generated module $M_i$; by [F4] every point of $X$ lies in such a chart, so this family covers $X$, and it is the family of all such charts, determined without selecting anything.

For every chart $U$ of the cover of step 1.2 the intersection $\mathrm{Supp}(\mathcal{F})\cap U$ is closed in $U$ by step 1.1, so its complement $U\setminus \mathrm{Supp}(\mathcal{F})$ is open in $U$, and since the $U$ cover $X$ the complement $X\setminus \mathrm{Supp}(\mathcal{F})={\bigcup }_U(U\setminus \mathrm{Supp}(\mathcal{F}))$ is open in $X$ by [F5]; hence $\mathrm{Supp}(\mathcal{F})$ is closed in $X$, as claimed.

The identification of the affine support with $V({\mathrm{Ann}}_A(M))$ is step 1.1, and the Axiom of Choice is used only through [F2], inherited from the associated-sheaf construction, and through the supplier [F3]; the cover of step 1.2 is the family of all admissible charts, so no selection occurs there.