Step
*
of Lemma
grp_inv_inv
∀[g:IGroup]. ∀[a:|g|]. ((~ (~ a)) = a ∈ |g|)
BY
{ UnivCD THENA Auto }
1
1. g : IGroup
2. a : |g|
⊢ (~ (~ a)) = a ∈ |g|
Latex:
Latex:
\mforall{}[g:IGroup]. \mforall{}[a:|g|]. ((\msim{} (\msim{} a)) = a)
By
Latex:
UnivCD THENA Auto
Home
Index