---

Step * of Lemma non-empty-bag-implies-non-void

∀[T:Type]. ∀[bs:bag(T)].  ((¬(bs = {} ∈ bag(T))) ⇒ (↓T))
BY
{ (Auto
   THEN (RWO "empty-bag-iff-size" (-1) THENA Auto)
   THEN (Assert 0 < #(bs) BY
               Auto)
   THEN (RWO "bag-member-iff-size<" (-1) THENA Auto)
   THEN SqExRepD
   THEN D 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].    ((\mneg{}(bs  =  \{\}))  {}\mRightarrow{}  (\mdownarrow{}T))


By

---

Latex:
(Auto
  THEN  (RWO  "empty-bag-iff-size"  (-1)  THENA  Auto)
  THEN  (Assert  0  <  \#(bs)  BY
                          Auto)
  THEN  (RWO  "bag-member-iff-size<"  (-1)  THENA  Auto)
  THEN  SqExRepD
  THEN  D  0
  THEN  Auto)

---

Home Index