---

Step * 1 1 of Lemma massoc_transitivity


1. g : IAbMonoid@i'
2. a : |g|@i
3. b : |g|@i
4. c : |g|@i
5. a ~ b@i
6. b ~ c@i
7. Refl(|g|;x,y.x ~ y)
8. Sym(|g|;x,y.x ~ y)
9. ∀a,b,c:|g|.  ((a ~ b) ⇒ (b ~ c) ⇒ (a ~ c))
⊢ a ~ c
BY
{ EAuto 1⋅ }

---

Latex:

---

Latex:

1.  g  :  IAbMonoid@i'
2.  a  :  |g|@i
3.  b  :  |g|@i
4.  c  :  |g|@i
5.  a  \msim{}  b@i
6.  b  \msim{}  c@i
7.  Refl(|g|;x,y.x  \msim{}  y)
8.  Sym(|g|;x,y.x  \msim{}  y)
9.  \mforall{}a,b,c:|g|.    ((a  \msim{}  b)  {}\mRightarrow{}  (b  \msim{}  c)  {}\mRightarrow{}  (a  \msim{}  c))
\mvdash{}  a  \msim{}  c


By

---

Latex:
EAuto  1\mcdot{}

---

Home Index