Closed points in fibres

Yesterday I found this in a preprint by Brian Osserman and Sam Payne:

  • If X —> S is locally of finite type, and x -> z is a specialization of points in X with z a closed point of its fibre, then there exist specializations x -> y, y -> z such that y is in the same fibre as x and is a closed point of it. Moreover, the set of all such y is dense in the closure of {x} in its fibre.

I was already planning to try to prove this and add it to the stacks project as I think that it could be quite useful.

To prove this statement you first reduce to the case where the base is a valuation ring and the morphism is flat. My idea was to use an argument a la Raynaud-Gruson to reduce to the case of a smooth morphism, where you can slice the map, i.e., argue by induction on the dimension. Brian and Sam’s argument is simpler: they show that you can do the slicing without reducing to a smooth morphism by showing that a locally principal closed subscheme which misses the generic fibre has to be “vertical”. This intermediate result is interesting by itself.

Does anybody have a reference for this, or similar, results? (I looked in EGA…)