---

Step * 1 of Lemma nwkl!-implies-fan


1. WKL!(𝔹)@i'
⊢ ∃k:ℕ. 𝔹 ~ ℕk
BY
{ (With ⌜2⌝ (D 0)⋅ THEN Auto THEN BLemma `equipollent-two`)⋅ }

---

Latex:

---

Latex:

1.  WKL!(\mBbbB{})@i'
\mvdash{}  \mexists{}k:\mBbbN{}.  \mBbbB{}  \msim{}  \mBbbN{}k


By

---

Latex:
(With  \mkleeneopen{}2\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  BLemma  `equipollent-two`)\mcdot{}

---

Home Index