---

Step * of Lemma nat_well_founded

WellFnd{i}(ℕ;x,y.x < y)
BY
{ UnfoldTopAb 0 }

1
∀[P:ℕ ⟶ ℙ]. ((∀j:ℕ. ((∀k:ℕ. (k < j ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:ℕ. P[n]})

---

Latex:

---

Latex:
WellFnd\{i\}(\mBbbN{};x,y.x  <  y)


By

---

Latex:
UnfoldTopAb  0

---

Home Index