---

Step * of Lemma add_grp_of_rng_wf_a

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

1
1. r : Rng
⊢ r↓+gp ∈ Group{i}

---

Latex:

---

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


By

---

Latex:
((D  0)  THENA  Auto)

---

Home Index