[Agda] ℕ ⊆ P U Q -> ¬ isFinite P or ...

[Sergei Meshveliani]

People,

I have been asked about a constructive proof of this theorem:

  ℕ ⊆ P U Q -> (¬ isFinite P) ⊎ (¬ isFinite Q).


A subset in ℕ is defined as an algorithmic predicate  P : ℕ -> Set.

setℕ (total set),  _⊆_,  P,  _U_ (union)  
are defined in a natural way, via predicates.

Finiteness is defined as 

  _Enumerates_ : List ℕ → NSet → Set _
  xs Enumerates P =
                    {x : ℕ} → P x → x ∈ xs

  isFinite : NSet → Set _
  isFinite P =  ∃ \xs → xs Enumerates P


I have proved this in Agda:

 ⋃isFiniteIfBoth : {P Q : NSet} → isFinite P → isFinite Q → 
                                               isFinite (P ⋃ Q),

 theorem1 : {P Q : NSet} → setℕ ⊆ (P ⋃ Q) → ¬ (isFinite P × isFinite Q).


And I have an impression that the statement 

 question : {P Q : NSet} → setℕ ⊆ (P ⋃ Q) → 
                                       (¬ isFinite P) ⊎ (¬ isFinite Q)

has not a constructive proof.

Has it?

Thanks,

------
Sergei