---

Step * of Lemma add_grp_of_rng_wf

∀[r:RngSig]. (r↓+gp ∈ GrpSig)
BY
{ Unfolds ``add_grp_of_rng grp_sig`` 0 THEN Auto }

---

Latex:

---

Latex:
\mforall{}[r:RngSig].  (r\mdownarrow{}+gp  \mmember{}  GrpSig)


By

---

Latex:
Unfolds  ``add\_grp\_of\_rng  grp\_sig``  0  THEN  Auto

---

Home Index