---

Step * 1 of Lemma cosetTC_functionality_subset


1. a : coSet{i:l}
2. b : coSet{i:l}
3. ∀x:coSet{i:l}. ((x ∈ a) ⇒ (x ∈ b))
4. x : coSet{i:l}
5. (x ∈ cosetTC(a))
⊢ (x ∈ cosetTC(b))
BY
{ ((SetMemDef (-1) THEN SetMemDef 0)
   THEN (Assert ⌜∃p:{p:copath(T.T;b)| 0 < copath-length(p)} . seteq(copath-at(a;t);copath-at(b;p))⌝⋅
   THENM (ParallelLast THEN Auto)
   )
   THEN ThinVar `x') }

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

---

Latex:

---

Latex:

1.  a  :  coSet\{i:l\}
2.  b  :  coSet\{i:l\}
3.  \mforall{}x:coSet\{i:l\}.  ((x  \mmember{}  a)  {}\mRightarrow{}  (x  \mmember{}  b))
4.  x  :  coSet\{i:l\}
5.  (x  \mmember{}  cosetTC(a))
\mvdash{}  (x  \mmember{}  cosetTC(b))


By

---

Latex:
((SetMemDef  (-1)  THEN  SetMemDef  0)
  THEN  (Assert  \mkleeneopen{}\mexists{}p:\{p:copath(T.T;b)|  0  <  copath-length(p)\}  .  seteq(copath-at(a;t);copath-at(b;p))\mkleeneclose{}\mcdot{}
  THENM  (ParallelLast  THEN  Auto)
  )
  THEN  ThinVar  `x')

---

Home Index