WellFnd{i}(ℕ;x,y.x < y)
{ UnfoldTopAb 0 }
∀[P:ℕ ⟶ ℙ]. ((∀j:ℕ. ((∀k:ℕ. (k < j
P[k]))
P[j]))
{∀n:ℕ. P[n]})