Разрешимость $\forall \exists $-теории некоторой фактор-решетки рекурсивно-перечислимых множеств

Доказывается разрешимость $\forall \exists $-теории решетки рекурсивно-перечислимых множеств, факторизованной по эквивалентности $X\sim Y\Leftrightarrow ((X\setminus Y)\cup(Y\setminus X))$ конечно или иммунно).