---

Step * of Lemma qadd_grp_wf2

No Annotations
<ℚ+> ∈ OGrp
BY
{ TACTIC:(MemTypeCD THENW Auto) }

1
<ℚ+> ∈ OCMon

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

---

Latex:

---

Latex:
No  Annotations
<\mBbbQ{}+>  \mmember{}  OGrp


By

---

Latex:
TACTIC:(MemTypeCD  THENW  Auto)

---

Home Index