---

Step * 1 2 1 1 1 of Lemma equipollent-nat-rationals

.....assertion..... 
ℕ+ ~ {1...}
BY
{ (With ⌜λx.x⌝ (D 0)⋅ THEN Auto) }

1
Bij(ℕ+;{1...};λx.x)

---

Latex:

---

Latex:
.....assertion..... 
\mBbbN{}\msupplus{}  \msim{}  \{1...\}


By

---

Latex:
(With  \mkleeneopen{}\mlambda{}x.x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index