---

Step * of Lemma int_add_grp_wf2

<ℤ+> ∈ OGrp
BY
{ MemTypeCD THENW Auto }

1
<ℤ+> ∈ OCMon

2
.....set predicate..... 
Inverse(|<ℤ+>|;*;e;~)

---

Latex:

---

Latex:
<\mBbbZ{}+>  \mmember{}  OGrp


By

---

Latex:
MemTypeCD  THENW  Auto

---

Home Index