---

Step * 1 of Lemma bsubmset_transitivity


∀s:DSet. ∀a,b,c:|s| List.
  ((↑(mk_mset(a) ⊆b mk_mset(b))) ⇒ (↑(mk_mset(b) ⊆b mk_mset(c))) ⇒ (↑(mk_mset(a) ⊆b mk_mset(c))))
BY
{ ((RepD THENM All (RWW "bsubmset_elim") 
THENM RelRST) THEN Auto) }

---

Latex:

---

Latex:

\mforall{}s:DSet.  \mforall{}a,b,c:|s|  List.
    ((\muparrow{}(mk\_mset(a)  \msubseteq{}\msubb{}  mk\_mset(b)))  {}\mRightarrow{}  (\muparrow{}(mk\_mset(b)  \msubseteq{}\msubb{}  mk\_mset(c)))  {}\mRightarrow{}  (\muparrow{}(mk\_mset(a)  \msubseteq{}\msubb{}  mk\_mset(c))))


By

---

Latex:
((RepD  THENM  All  (RWW  "bsubmset\_elim") 
THENM  RelRST)  THEN  Auto)

---

Home Index