---

Step * of Lemma bag-filter-filter

∀[p,q,bs:Top].  ([x∈[x∈bs|p[x]]|q[x]] ~ [x∈bs|p[x] ∧b q[x]])
BY
{ (Unfold `bag-filter` 0 THEN (RWO "filter-filter" 0 THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p,q,bs:Top].    ([x\mmember{}[x\mmember{}bs|p[x]]|q[x]]  \msim{}  [x\mmember{}bs|p[x]  \mwedge{}\msubb{}  q[x]])


By

---

Latex:
(Unfold  `bag-filter`  0  THEN  (RWO  "filter-filter"  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index