---

Step * of Lemma mset_fact

∀s:DSet. ∀a:MSet{s}.  (a = (msFor{mset_mon{s}} x ∈ a. mset_inj{s}(x)) ∈ MSet{s})
BY
{ ((D 0) THENA Auto) }

1
1. s : DSet
⊢ ∀a:MSet{s}. (a = (msFor{mset_mon{s}} x ∈ a. mset_inj{s}(x)) ∈ MSet{s})

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a:MSet\{s\}.    (a  =  (msFor\{mset\_mon\{s\}\}  x  \mmember{}  a.  mset\_inj\{s\}(x)))


By

---

Latex:
((D  0)  THENA  Auto)

---

Home Index