---

Step * of Lemma ccc-nset-transparent

∀K:Type. (CCCNSet(K) ⇒ Transparent(K))
BY
{ (Auto THEN RepeatFor 2 (D -1) THEN RenameVar `k0' (-2) THEN D 0 THEN Auto) }

1
1. K : Type
2. K ⊆r ℕ
3. k0 : K
4. CCC(K)
5. B : ℕ
⊢ (∀k:K. (k ≤ B)) ∨ (∃k:K. B < k)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  -1)  THEN  RenameVar  `k0'  (-2)  THEN  D  0  THEN  Auto)

---

Home Index