---

Step * of Lemma assert-bag-null-sq

∀bs:bag(Top). ((↑bag-null(bs)) ⇒ (bs ~ {}))
BY
{ (Auto THEN (RWO "assert-bag-null" (-1) THEN Auto) THEN FLemma `equal-empty-bag` [-1] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}bs:bag(Top).  ((\muparrow{}bag-null(bs))  {}\mRightarrow{}  (bs  \msim{}  \{\}))


By

---

Latex:
(Auto  THEN  (RWO  "assert-bag-null"  (-1)  THEN  Auto)  THEN  FLemma  `equal-empty-bag`  [-1]  THEN  Auto)

---

Home Index