---

Step * 1 1 1 1 1 of Lemma cosetTC-least


1. s : coSet{i:l}
2. transitive-set(s)
3. n : ℤ
4. [%2] : 0 < n
5. 0 < n - 1 ⇒ (∀x:coSet{i:l}. ((x ⊆ s) ⇒ (∀p:coPath(T.T;x;n - 1). (coPath-at(n - 1;x;p) ∈ s))))
6. 0 < n
7. x : coSet{i:l}
8. (x ⊆ s)
9. p : coPath(T.T;x;n)
⊢ (coPath-at(n;x;p) ∈ s)
BY
{ (MoveToConcl (-1) THEN Unfold `coPath` 0 THEN Unfold `coPath-at` 0 THEN AutoSplit THEN Auto THEN D -1 THEN Reduce 0) }

1
1. s : coSet{i:l}
2. transitive-set(s)
3. n : ℤ
4. n ≠ 0
5. [%2] : 0 < n
6. 0 < n - 1 ⇒ (∀x:coSet{i:l}. ((x ⊆ s) ⇒ (∀p:coPath(T.T;x;n - 1). (coPath-at(n - 1;x;p) ∈ s))))
7. 0 < n
8. x : coSet{i:l}
9. (x ⊆ s)
10. t : coW-dom(T.T;x)
11. p1 : coPath(T.T;coW-item(x;t);n - 1)
⊢ (coPath-at(n - 1;coW-item(x;t);p1) ∈ s)

---

Latex:

---

Latex:

1.  s  :  coSet\{i:l\}
2.  transitive-set(s)
3.  n  :  \mBbbZ{}
4.  [\%2]  :  0  <  n
5.  0  <  n  -  1  {}\mRightarrow{}  (\mforall{}x:coSet\{i:l\}.  ((x  \msubseteq{}  s)  {}\mRightarrow{}  (\mforall{}p:coPath(T.T;x;n  -  1).  (coPath-at(n  -  1;x;p)  \mmember{}  s))))
6.  0  <  n
7.  x  :  coSet\{i:l\}
8.  (x  \msubseteq{}  s)
9.  p  :  coPath(T.T;x;n)
\mvdash{}  (coPath-at(n;x;p)  \mmember{}  s)


By

---

Latex:
(MoveToConcl  (-1)
  THEN  Unfold  `coPath`  0
  THEN  Unfold  `coPath-at`  0
  THEN  AutoSplit
  THEN  Auto
  THEN  D  -1
  THEN  Reduce  0)

---

Home Index