---

Step * 1 of Lemma bag-size-bag-member


1. T : Type
2. bs : T List
3. ∃b:T. b ↓∈ bs
⊢ 0 < #(bs)
BY
{ RepeatFor 2 ((D (-1) THEN ExRepD)) }

1
1. T : Type
2. bs : T List
3. b : T
4. L : T List
5. L = bs ∈ bag(T)
6. (b ∈ L)
⊢ 0 < #(bs)

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  T  List
3.  \mexists{}b:T.  b  \mdownarrow{}\mmember{}  bs
\mvdash{}  0  <  \#(bs)


By

---

Latex:
RepeatFor  2  ((D  (-1)  THEN  ExRepD))

---

Home Index