---

Step * of Lemma bsubmset_transitivity

∀s:DSet. ∀a,b,c:MSet{s}.  ((↑(a ⊆b b)) ⇒ (↑(b ⊆b c)) ⇒ (↑(a ⊆b c)))
BY
{ ((RW mset_elimC 0) THENA Auto) }

1
∀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))))

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a,b,c:MSet\{s\}.    ((\muparrow{}(a  \msubseteq{}\msubb{}  b))  {}\mRightarrow{}  (\muparrow{}(b  \msubseteq{}\msubb{}  c))  {}\mRightarrow{}  (\muparrow{}(a  \msubseteq{}\msubb{}  c)))


By

---

Latex:
((RW  mset\_elimC  0)  THENA  Auto)

---

Home Index