---

Step * of Lemma quot_grp_inv_wf

∀g:IGroup. ∀h:NormSubGrp{i}(g).  (~ ∈ |g//h| ⟶ |g//h|)
BY
{ ((UnivCD THENA Auto) THEN D -1) }

1
1. g : IGroup
2. h : |g| ⟶ ℙ
3. h SubGrp of g ∧ norm_subset_p(g;h)
⊢ ~ ∈ |g//h| ⟶ |g//h|

---

Latex:

---

Latex:
\mforall{}g:IGroup.  \mforall{}h:NormSubGrp\{i\}(g).    (\msim{}  \mmember{}  |g//h|  {}\mrightarrow{}  |g//h|)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  -1)

---

Home Index