---

Step * of Lemma omral_zero_wf

∀g:OCMon. ∀r:CDRng.  (00g,r ∈ |omral(g;r)|)
BY
{ (((Unfolds ``omral_zero omralist`` 0) THEN Auto) THEN BLemma `cdrng_is_abdmonoid` THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(((Unfolds  ``omral\_zero  omralist``  0)  THEN  Auto)  THEN  BLemma  `cdrng\_is\_abdmonoid`  THEN  Auto)

---

Home Index