On using Lazard's projection in CAD construction

In 1994 Lazard proposed an improved projection operation for cylindrical algebraic decomposition (CAD). For the proof he introduced a certain notion of valuation of a multivariate Puiseux series at a point. However a gap in one of the key supporting results for the improved projection was subsequently noticed. In this paper we show that Lazard's projection is valid for CAD construction for so-called well-oriented polynomial sets. Our proof does not make use of Lazard's notion of valuation, however.