 Quantifier elimination for dense linear orders without endpoints

The theory of dense linear orders without endpoints eliminates quantifiers. A finite partial order isomorphism extends by placing each new point in the corresponding interval or ray.