---

Step * 1 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(n;s;t1) ∈ s)
BY
{ ((Assert ⌜∀x:coSet{i:l}. ((x ⊆ s) ⇒ (∀p:coPath(T.T;x;n). (coPath-at(n;x;p) ∈ s)))⌝⋅
   THENM (InstHyp [⌜s⌝;⌜t1⌝] (-1)⋅ THEN EAuto 1)
   )
   THEN Thin (-2)
   ) }

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

---

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(n;s;t1)  \mmember{}  s)


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}x:coSet\{i:l\}.  ((x  \msubseteq{}  s)  {}\mRightarrow{}  (\mforall{}p:coPath(T.T;x;n).  (coPath-at(n;x;p)  \mmember{}  s)))\mkleeneclose{}\mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}s\mkleeneclose{};\mkleeneopen{}t1\mkleeneclose{}]  (-1)\mcdot{}  THEN  EAuto  1)
  )
  THEN  Thin  (-2)
  )

---

Home Index