---

Step * 1 of Lemma fan-iff-wkl!

.....antecedent..... 
∃k:ℕ. 𝔹 ~ ℕk
BY
{ (With ⌜2⌝ (D 0)⋅ THEN Auto THEN BLemma `equipollent-two`)⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
\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