---

Step * of Lemma ideal_wf

∀[r:CRng]. (Ideal(r){i} ∈ 𝕌')
BY
{ Unfold `ideal` 0 THEN Auto }

---

Latex:

---

Latex:
\mforall{}[r:CRng].  (Ideal(r)\{i\}  \mmember{}  \mBbbU{}')


By

---

Latex:
Unfold  `ideal`  0  THEN  Auto

---

Home Index