---

Step * 1 2 of Lemma add_grp_of_rng_wf_b

.....set predicate..... 
1. r : Rng
⊢ Comm(|r↓+gp|;*)
BY
{ AbReduce 0  
THEN Unfold `comm` 0 }

1
1. r : Rng
⊢ ∀[x,y:|r|].  ((x +r y) = (y +r x) ∈ |r|)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  r  :  Rng
\mvdash{}  Comm(|r\mdownarrow{}+gp|;*)


By

---

Latex:
AbReduce  0   
THEN  Unfold  `comm`  0

---

Home Index