---

Step * of Lemma ccc-nset-weakly-decidable

∀K:Type. (CCCNSet(K) ⇒ WD(K))
BY
{ (Auto THEN D 0) }

1
1. K : Type
2. CCCNSet(K)
⊢ K ⊆r ℕ

2
1. K : Type
2. CCCNSet(K)
⊢ ∀m,k:K. ∀l:{m..k-}.  ((l ∈ K) ∨ (¬(l ∈ K)))

---

Latex:

---

Latex:
\mforall{}K:Type.  (CCCNSet(K)  {}\mRightarrow{}  WD(K))


By

---

Latex:
(Auto  THEN  D  0)

---

Home Index