---

Step * 1 1 1 1 of Lemma cosetTC-least


1. s : coSet{i:l}
2. transitive-set(s)
3. n : ℕ
4. 0 < n
⊢ ∀x:coSet{i:l}. ((x ⊆ s) ⇒ (∀p:coPath(T.T;x;n). (coPath-at(n;x;p) ∈ s)))
BY
{ (NatInd (-2) THEN Auto THEN Try ((Unfold `coSet` 0 THEN Auto))) }

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

---

Latex:

---

Latex:

1.  s  :  coSet\{i:l\}
2.  transitive-set(s)
3.  n  :  \mBbbN{}
4.  0  <  n
\mvdash{}  \mforall{}x:coSet\{i:l\}.  ((x  \msubseteq{}  s)  {}\mRightarrow{}  (\mforall{}p:coPath(T.T;x;n).  (coPath-at(n;x;p)  \mmember{}  s)))


By

---

Latex:
(NatInd  (-2)  THEN  Auto  THEN  Try  ((Unfold  `coSet`  0  THEN  Auto)))

---

Home Index