---

Step * of Lemma bsublist_transitivity

∀s:DSet. ∀us,vs,ws:|s| List.  ((↑bsublist(s;us;vs)) ⇒ (↑bsublist(s;vs;ws)) ⇒ (↑bsublist(s;us;ws)))
BY
{ (UnivCD THENA Auto) }

1
1. s : DSet@i'
2. us : |s| List@i
3. vs : |s| List@i
4. ws : |s| List@i
5. ↑bsublist(s;us;vs)@i
6. ↑bsublist(s;vs;ws)@i
⊢ ↑bsublist(s;us;ws)

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}us,vs,ws:|s|  List.    ((\muparrow{}bsublist(s;us;vs))  {}\mRightarrow{}  (\muparrow{}bsublist(s;vs;ws))  {}\mRightarrow{}  (\muparrow{}bsublist(s;us;ws)))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index