---

Step * of Lemma grp_inv_id

∀[g:IGroup]. ((~ e) = e ∈ |g|)
BY
{ D 0 THENA Auto }

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

---

Latex:

---

Latex:
\mforall{}[g:IGroup].  ((\msim{}  e)  =  e)


By

---

Latex:
D  0  THENA  Auto

---

Home Index