---

Step * of Lemma grp_id_wf2

∀[g:OGrp]. (e ∈ |g|+)
BY
{ ((D 0 THENM MemTypeCD) THEN Auto) }

1
.....set predicate..... 
1. g : OGrp
⊢ e ≤ e

---

Latex:

---

Latex:
\mforall{}[g:OGrp].  (e  \mmember{}  |g|\msupplus{})


By

---

Latex:
((D  0  THENM  MemTypeCD)  THEN  Auto)

---

Home Index