By constructive mathematics in this matter we mean ZF without the law of the excluded third (*). In the language of [locales](https://ncatlab.org/nlab/show/locale), the Jordan curve can be defined as $f\colon I \to X$ such that "if $U \cap V = \varnothing$, then $f(U) \cap f(V) = \varnothing$" (coincides with the classical definition for Hausdorff spaces). So, is Jordan's theorem true for locales in constructive mathematics? (*) I like Martin-Löf's intuitionistic theory of types more and it seems that in a sense "this is the same question", but I have not studied the type theory systematically yet, so I am formulating the question in a more familiar language.