---

Step * of Lemma cosetTC-transitive

∀a:coSet{i:l}. transitive-set(cosetTC(a))
BY
{ ((RWO "transitive-set-iff" 0 THENA Auto)
   THEN RWO "setsubset-iff" 0
   THEN Auto
   THEN SetMemDef (-3)
   THEN SetMemDef 0
   THEN (RWO "-3" (-1) THENA Auto)
   THEN ThinVar `x') }

1
1. a : coSet{i:l}
2. t : {p:copath(T.T;a)| 0 < copath-length(p)} 
3. x1 : coSet{i:l}
4. (x1 ∈ copath-at(a;t))
⊢ ∃t:{p:copath(T.T;a)| 0 < copath-length(p)} . seteq(x1;copath-at(a;t))

---

Latex:

---

Latex:
\mforall{}a:coSet\{i:l\}.  transitive-set(cosetTC(a))


By

---

Latex:
((RWO  "transitive-set-iff"  0  THENA  Auto)
  THEN  RWO  "setsubset-iff"  0
  THEN  Auto
  THEN  SetMemDef  (-3)
  THEN  SetMemDef  0
  THEN  (RWO  "-3"  (-1)  THENA  Auto)
  THEN  ThinVar  `x')

---

Home Index