О разрешимости теории конечных подмножеств для дискретного линейного порядка

Мы рассматриваем метод построения новых алгебраических систем как конечных подмножеств уже существующих. Берем исходные системы, обладающие дискретным линейным порядком, и вводим на них новое отношение для конечных подмножеств. Считаем, что два подмножества состоят в новом отношении тогда и только тогда, когда каждый элемент первого подмножества меньше каждого элемента второго. Для теорий таких систем мы доказываем, что они допускают эффективную элиминацию кванторов. Следовательно, такие теории являются разрешимыми.