---

Step * 3 of Lemma seteq_equiv


1. Sym(coSet{i:l};s1,s2.seteq(s1;s2))
2. a : coSet{i:l}
3. b : coSet{i:l}
4. c : coSet{i:l}
5. seteq(a;b)
6. seteq(b;c)
⊢ seteq(a;c)
BY
{ (UseTrans ⌜b⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  Sym(coSet\{i:l\};s1,s2.seteq(s1;s2))
2.  a  :  coSet\{i:l\}
3.  b  :  coSet\{i:l\}
4.  c  :  coSet\{i:l\}
5.  seteq(a;b)
6.  seteq(b;c)
\mvdash{}  seteq(a;c)


By

---

Latex:
(UseTrans  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index