---

Step * 1 1 2 of Lemma oal_grp_wf2

.....set predicate..... 
1. s : LOSet@i'
2. g : OGrp@i'
3. oal_grp(s;g) ∈ AbGrp
4. oal_grp(s;g) ∈ OMon
⊢ Inverse(|oal_grp(s;g)|;*;e;~)
BY
{ Thin (-1) }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. oal_grp(s;g) ∈ AbGrp
⊢ Inverse(|oal_grp(s;g)|;*;e;~)

---

Latex:

---

Latex:
.....set  predicate..... 
1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  oal\_grp(s;g)  \mmember{}  AbGrp
4.  oal\_grp(s;g)  \mmember{}  OMon
\mvdash{}  Inverse(|oal\_grp(s;g)|;*;e;\msim{})


By

---

Latex:
Thin  (-1)

---

Home Index