---

Step * of Lemma rng_plus_comm

∀[r:Rng]. ∀[a,b:|r|].  ((a +r b) = (b +r a) ∈ |r|)
BY
{ ((UnivCD) THENA Auto) }

1
1. r : Rng
2. a : |r|
3. b : |r|
⊢ (a +r b) = (b +r a) ∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:Rng].  \mforall{}[a,b:|r|].    ((a  +r  b)  =  (b  +r  a))


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index