Regular Separability of Well-Structured Transition Systems

We investigate languages recognized by well-structured transition systems (WSTS), 
i.e., infinite systems with state space ordered by a well quasi-order (WQO).
We show that, surprisingly, under very mild assumptions every two disjoint WSTS
languages are regularly separable: There is a regular language containing one of them and 
disjoint from the other. As a consequence, if a language, as well as its complement,
both are recognized by a WSTS, then they are necessarily regular.