---

Step * of Lemma mset_mem_char

No Annotations
∀s:DSet. ∀x:|s|. ∀a:MSet{s}.  x ∈b a = ∃b{s} y ∈ a. (y (=b) x)
BY
{ ((RepD THENM OnVar `a' msetD 
THENM Unfolds ``mset_mem mset_for`` 0) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}s:DSet.  \mforall{}x:|s|.  \mforall{}a:MSet\{s\}.    x  \mmember{}\msubb{}  a  =  \mexists{}\msubb{}\{s\}  y  \mmember{}  a.  (y  (=\msubb{})  x)


By

---

Latex:
((RepD  THENM  OnVar  `a'  msetD 
THENM  Unfolds  ``mset\_mem  mset\_for``  0)  THEN  Auto)

---

Home Index