---

Step * of Lemma es-decl-sets-sub_wf

∀[dd1,dd2:DeclSet].  (dd1 ⊆ dd2 ∈ ℙ')
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[dd1,dd2:DeclSet].    (dd1  \msubseteq{}  dd2  \mmember{}  \mBbbP{}')


By

---

Latex:
Auto

---

Home Index