---

Step * of Lemma dset_of_mon_wf2

∀[g:OMon]. (g↓set ∈ LOSet)
BY
{ Fold `oset_of_ocmon` 0  
THEN Lemma `oset_of_ocmon_wf` }

---

Latex:

---

Latex:
\mforall{}[g:OMon].  (g\mdownarrow{}set  \mmember{}  LOSet)


By

---

Latex:
Fold  `oset\_of\_ocmon`  0   
THEN  Lemma  `oset\_of\_ocmon\_wf`

---

Home Index