---

Step * of Lemma oal_hgp_wf

∀s:LOSet. ∀g:OGrp.  (oal_hgp(s;g) ∈ GrpSig)
BY
{ (Auto THEN (Assert g↓hgrp ∈ OCMon BY Auto) THEN Unfolds ``oal_hgp grp_sig`` 0⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.    (oal\_hgp(s;g)  \mmember{}  GrpSig)


By

---

Latex:
(Auto  THEN  (Assert  g\mdownarrow{}hgrp  \mmember{}  OCMon  BY  Auto)  THEN  Unfolds  ``oal\_hgp  grp\_sig``  0\mcdot{}  THEN  Auto)

---

Home Index