---

Step * 1 of Lemma grp_inv_id


1. g : IGroup
⊢ (~ e) = e ∈ |g|
BY
{ RWN 2 (RevGenLemmaWithThenLC 1 [`a',e] 
         [] `grp_inverse`) 0 
THENA Auto }

1
1. g : IGroup
⊢ (~ e) = (e * (~ e)) ∈ |g|

---

Latex:

---

Latex:

1.  g  :  IGroup
\mvdash{}  (\msim{}  e)  =  e


By

---

Latex:
RWN  2  (RevGenLemmaWithThenLC  1  [`a',e] 
                  []  `grp\_inverse`)  0 
THENA  Auto

---

Home Index