---

Step * of Lemma hgrp_of_ocgrp_wf2

∀[g:OGrp]. (g↓hgrp ∈ OCMon)
BY
{ ((D 0 THENM BLemma `inj_into_ocmon`) THENA Auto) }

1
1. g : OGrp
⊢ ∃h:OCMon
   ∃f:|(g↓hgrp)| ⟶ |h|
    (IsMonHomInj(g↓hgrp;h;f)
    ∧ RelsIso(|(g↓hgrp)|;|h|;x,y.↑(x =b y);x,y.↑(x =b y);f)
    ∧ RelsIso(|(g↓hgrp)|;|h|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);f))

---

Latex:

---

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


By

---

Latex:
((D  0  THENM  BLemma  `inj\_into\_ocmon`)  THENA  Auto)

---

Home Index