---

Step * of Lemma inductive-set_wf

∀[R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ']. ∀[bdd:Bounded(x,a.R[x;a])].  (inductive-set(bdd) ∈ Set{i:l})
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[R:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[bdd:Bounded(x,a.R[x;a])].    (inductive-set(bdd)  \mmember{}  Set\{i:l\})


By

---

Latex:
ProveWfLemma

---

Home Index