On decidability of finite subsets’ theory for discrete linear order

Let us consider a discrete linear ordered set. On finite subsets of such set we introduce a new binary relation. This relation says that all items of a first set is less than all items of a second one. We show that the theory of such constructed structure admits quantifier elimination. For this purpose, we expand the language with four definable functions. As a corollary we get the theory of finite subsets of a discrete linear order to be decidable.