---

Step * 1 1 1 of Lemma grp_inv_inv


1. g : IGroup
2. a : |g|
⊢ e = e ∈ |g|
BY
{ Auto }

---

Latex:

---

Latex:

1.  g  :  IGroup
2.  a  :  |g|
\mvdash{}  e  =  e


By

---

Latex:
Auto

---

Home Index