---

Step * of Lemma omralist_wf

∀g:OCMon. ∀r:CDRng.  (omral(g;r) ∈ DSet)
BY
{ (Intros THEN (Assert r↓+gp ∈ AbDMon BY (BLemma `cdrng_is_abdmonoid` THEN Auto)) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}g:OCMon.  \mforall{}r:CDRng.    (omral(g;r)  \mmember{}  DSet)


By

---

Latex:
(Intros  THEN  (Assert  r\mdownarrow{}+gp  \mmember{}  AbDMon  BY  (BLemma  `cdrng\_is\_abdmonoid`  THEN  Auto))  THEN  ProveWfLemma)

---

Home Index