A flat local map is faithfully flat

Let $\phi :(A,\mathfrak{m})\to (B,\mathfrak{n})$ be a local homomorphism of nonzero local rings, that is $\phi (\mathfrak{m})\subseteq \mathfrak{n}$, and assume $B$ flat as an $A$-module. If $I⊊A$ is a proper ideal, then $I\subseteq \mathfrak{m}$ by [F1], hence $IB\subseteq \mathfrak{m}B\subseteq \mathfrak{n}⊊B$ because $\mathfrak{n}$ is a proper ideal of the nonzero ring $B$; in particular $IB\mathrm{\ne }B$.

We claim that $N{\otimes }_{A}B\mathrm{\ne }0$ for every nonzero $A$-module $N$. Choose $0\mathrm{\ne }x\in N$ and put $\mathfrak{a}={\mathrm{Ann}}_A(x)=\{a:ax=0\}$, a proper ideal of $A$ since $1\mathrm{\notin }\mathfrak{a}$; by [F1] $\mathfrak{a}\subseteq \mathfrak{m}$. The $A$-linear map $A\mathrm{/}\mathfrak{a}\to N$, $\bar{a}\mapsto ax$, is injective with nonzero image, and $(A\mathrm{/}\mathfrak{a}){\otimes }_{A}B\cong B\mathrm{/}\mathfrak{a}B$, which is nonzero because $\mathfrak{a}B\subseteq \mathfrak{m}B\subseteq \mathfrak{n}⊊B$ as in step 1.1. Since $B$ is flat, [F4] makes the induced map $B\mathrm{/}\mathfrak{a}B\to N{\otimes }_{A}B$ injective, so $N{\otimes }_{A}B\mathrm{\ne }0$. The containment of $\mathfrak{a}$ in $\mathfrak{m}$ uses the AC-qualified assertion in [F1].

By the equivalence of [F3] applied to the flat $A$-module $B$, the nonvanishing proved in step 2.1 is exactly the second condition, so $B$ is faithfully flat over $A$. The assumed AC licenses [F3] and, separately, the proper-ideal containment in [F1].

Now let $f:X\to S$ be flat at a point $x\in X$ and put $s=f(x)$. By [F5] the local ring map ${\mathcal{O}}_{S,s}\to {\mathcal{O}}_{X,x}$ is flat, and by [F5] and [F1] the two rings are nonzero local rings; applying step 3.1 to this local homomorphism gives that ${\mathcal{O}}_{X,x}$ is faithfully flat over ${\mathcal{O}}_{S,s}$, which is the geometric assertion. [F1, F5, step 3.1] $\mathrm{\square }$