---

Step * of Lemma seteq_equiv

EquivRel(coSet{i:l};s1,s2.seteq(s1;s2))
BY
{ RepeatFor 2 ((D 0 THEN Auto)) }

1
1. a : coSet{i:l}
⊢ seteq(a;a)

2
1. a : coSet{i:l}
2. b : coSet{i:l}
3. seteq(a;b)
⊢ seteq(b;a)

3
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)

---

Latex:

---

Latex:
EquivRel(coSet\{i:l\};s1,s2.seteq(s1;s2))


By

---

Latex:
RepeatFor  2  ((D  0  THEN  Auto))

---

Home Index