---

Step * 1 of Lemma bag-member-classfun


1. T : Type
2. b : bag(T)@i
⊢ single-valued-bag(b;T) ⇒ (1 ≤ #(b)) ⇒ sv-bag-only(b) ↓∈ b
BY
{ (Auto THEN BLemma `bag-member-sv-bag-only` THEN Auto) }

---

Latex:



1.  T  :  Type
2.  b  :  bag(T)@i
\mvdash{}  single-valued-bag(b;T)  {}\mRightarrow{}  (1  \mleq{}  \#(b))  {}\mRightarrow{}  sv-bag-only(b)  \mdownarrow{}\mmember{}  b


By

(Auto  THEN  BLemma  `bag-member-sv-bag-only`  THEN  Auto)

---

Home Index