---

Step * 1 of Lemma grp_inv_inv


1. g : IGroup
2. a : |g|
⊢ (~ (~ a)) = a ∈ |g|
BY
{ Using [`a',~ a]  
  (BackThruLemma `grp_op_cancel_l`) 
THENA Auto }

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

---

Latex:

---

Latex:

1.  g  :  IGroup
2.  a  :  |g|
\mvdash{}  (\msim{}  (\msim{}  a))  =  a


By

---

Latex:
Using  [`a',\msim{}  a]   
    (BackThruLemma  `grp\_op\_cancel\_l`) 
THENA  Auto

---

Home Index