Let $\mathrm{K}$ be the class of strict dense linear orders. Define $\Phi$ to be the following set of formulae: \begin{equation*} \{ \exists x \forall y : x = y \vee x < y, \exists x \forall y : x = y \vee y < x, \forall y : x = y \vee x < y, \forall y : x = y \vee y < x, x < y\}. \end{equation*}
Prove that $\Phi$ is an elimination set for $\mathrm{K}$.
So I know that the general idea is to prove that every formula can be expressed as a Boolean combination of formulae from the elimination set.
I've seen the proof that strict dense linear orders WITHOUT endpoints admits quantifier elimination. In this proof, we use an inductive argument; we assume that every formula $\varphi$ can be expressed as $\exists x \psi$, where $\psi$ is quantifier free (in disjunctive normal form), and proceed from there. However, I'm finding it tricky to apply this process to my question, as now $\psi$ can be any Boolean combination of formulae from the elimination set. Is it sufficient to show that $\exists x \chi$ is a Boolean combination of formulae from $\Phi$ for every $\chi \in \Phi$?
Recently I've received the hint that we can use the fact that strict dense linear orders without endpoints admits quantifier elimination. So my guess is that we have to 'add' the endpoints back in, but I'm not sure how I would go about that.