## Pfaffian closure

Let $\R$ be an o-minimal expansion of the real field, and let $\R_1$ be the expansion of $\R$ by all Rolle leaves over $\R$. Theorem The expansion $\R_1$ of $\R$ is o-minimal. Proof. Let $\Lambda$ be the system of all Rolle sets over $\R$; by this post, $\Lambda$ satisfies Axioms 1–7 of this post. $\qed$…