---

Step * 1 of Lemma mem_bsublist_imp


1. s : DSet
2. as : |s| List
3. bs : |s| List
4. ∀c:|s|. ((c #∈ as) ≤ (c #∈ bs))
5. c : |s|
6. (c #∈ as) > 0
⊢ (c #∈ bs) > 0
BY
{ (With c (D 4) THEN Auto') }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  as  :  |s|  List
3.  bs  :  |s|  List
4.  \mforall{}c:|s|.  ((c  \#\mmember{}  as)  \mleq{}  (c  \#\mmember{}  bs))
5.  c  :  |s|
6.  (c  \#\mmember{}  as)  >  0
\mvdash{}  (c  \#\mmember{}  bs)  >  0


By

---

Latex:
(With  c  (D  4)  THEN  Auto')

---

Home Index