---

Step * 1 1 2 1 of Lemma empty-bag-iff-size

.....assertion..... 
1. T : Type
2. bs : bag(T)
3. #(bs) ≤ 0
4. x : T
5. x ↓∈ bs
⊢ 0 < #(bs)
BY
{ (BLemma `bag-member-iff-size` ⋅ THEN Auto THEN D 0 THEN With ⌜x⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  bs  :  bag(T)
3.  \#(bs)  \mleq{}  0
4.  x  :  T
5.  x  \mdownarrow{}\mmember{}  bs
\mvdash{}  0  <  \#(bs)


By

---

Latex:
(BLemma  `bag-member-iff-size`  \mcdot{}  THEN  Auto  THEN  D  0  THEN  With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index