---

Step * of Lemma null_mset_wf_f

∀s:DSet. (0{s} ∈ FiniteSet{s})
BY
{ ((D 0 THENM MemTypeCD) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s:DSet.  (0\{s\}  \mmember{}  FiniteSet\{s\})


By

---

Latex:
((D  0  THENM  MemTypeCD)  THEN  Auto)

---

Home Index