---

Step * 1 1 of Lemma grp_inv_id


1. g : IGroup
⊢ (~ e) = (e * (~ e)) ∈ |g|
BY
{ RWH (GenLemmaC 2 `mon_ident`) 0 THEN Auto }

---

Latex:

---

Latex:

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


By

---

Latex:
RWH  (GenLemmaC  2  `mon\_ident`)  0  THEN  Auto

---

Home Index