Decision Problem for Separated Distributive Lattices

It is well known that for all recursively enumerable sets X₁, X₂ there are disjoint recursively enumerable sets Y₁, Y₂ such that Y_i is a subset of X_i and (Y₁ ∪ Y₂) = (X₁ ∪ X₂). Alistair Lachlan called distributed lattices satisfying this property separated. He proved that the first-order theory of finite separated distributed lattices is decidable. We prove here that the first-order theory of all separated distributed lattices is undecidable.