---

Step * of Lemma hgrp_of_ocgrp_wf

∀[g:OGrp]. (g↓hgrp ∈ GrpSig)
BY
{ ((D 0 THENM Unfolds ``hgrp_of_ocgrp grp_sig`` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[g:OGrp].  (g\mdownarrow{}hgrp  \mmember{}  GrpSig)


By

---

Latex:
((D  0  THENM  Unfolds  ``hgrp\_of\_ocgrp  grp\_sig``  0)  THEN  Auto)

---

Home Index