---

Step * of Lemma massoc_equiv_rel

∀g:IAbMonoid. EquivRel(|g|;x,y.x ~ y)
BY
{ ((UnivCD) THEN Auto) 
THEN Unfold `massoc` 0 }

1
1. g : IAbMonoid@i'
⊢ EquivRel(|g|;x,y.Symmetrize(x,y.x | y;x;y))

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  EquivRel(|g|;x,y.x  \msim{}  y)


By

---

Latex:
((UnivCD)  THEN  Auto) 
THEN  Unfold  `massoc`  0

---

Home Index