---

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


1. T : Type
2. bs : bag(T)
⊢ uiff(bs = {} ∈ bag(T);#(bs) ≤ 0)
BY
{ (RWO "empty-bag-iff-no-member" 0 THENA Auto) }

1
1. T : Type
2. bs : bag(T)
⊢ uiff(∀x:T. (¬x ↓∈ bs);#(bs) ≤ 0)

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  bag(T)
\mvdash{}  uiff(bs  =  \{\};\#(bs)  \mleq{}  0)


By

---

Latex:
(RWO  "empty-bag-iff-no-member"  0  THENA  Auto)

---

Home Index