---

Step * of Lemma iseg_product_wf

∀[j:ℕ]. ∀[i:ℕj + 1].  (iseg_product(i;j) ∈ ℕ)
BY
{ (ProveWfLemma THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[j:\mBbbN{}].  \mforall{}[i:\mBbbN{}j  +  1].    (iseg\_product(i;j)  \mmember{}  \mBbbN{})


By

---

Latex:
(ProveWfLemma  THEN  Auto')

---

Home Index