---

Step * 1 1 of Lemma cosetTC-least


1. s : coSet{i:l}
2. transitive-set(s)
3. n : ℕ
4. t1 : coPath(T.T;s;n)
5. 0 < n
⊢ (copath-at(s;<n, t1>) ∈ s)
BY
{ RepUR ``copath-at`` 0 }

1
1. s : coSet{i:l}
2. transitive-set(s)
3. n : ℕ
4. t1 : coPath(T.T;s;n)
5. 0 < n
⊢ (coPath-at(n;s;t1) ∈ s)

---

Latex:

---

Latex:

1.  s  :  coSet\{i:l\}
2.  transitive-set(s)
3.  n  :  \mBbbN{}
4.  t1  :  coPath(T.T;s;n)
5.  0  <  n
\mvdash{}  (copath-at(s;<n,  t1>)  \mmember{}  s)


By

---

Latex:
RepUR  ``copath-at``  0

---

Home Index