---

Step * of Lemma add_grp_of_rng_wf_b

∀[r:Rng]. (r↓+gp ∈ AbGrp)
BY
{ ((D 0) THENA Auto) }

1
1. r : Rng
⊢ r↓+gp ∈ AbGrp

---

Latex:

---

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


By

---

Latex:
((D  0)  THENA  Auto)

---

Home Index