---

Step * 1 of Lemma oal_grp_wf2


1. s : LOSet@i'
2. g : OGrp@i'
⊢ oal_grp(s;g) ∈ OGrp
BY
{ (((Assert oal_grp(s;g) ∈ AbGrp) THENA Auto) THEN ((Assert oal_grp(s;g) ∈ OMon) THENA Auto)) }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. oal_grp(s;g) ∈ AbGrp
4. oal_grp(s;g) ∈ OMon
⊢ oal_grp(s;g) ∈ OGrp

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
\mvdash{}  oal\_grp(s;g)  \mmember{}  OGrp


By

---

Latex:
(((Assert  oal\_grp(s;g)  \mmember{}  AbGrp)  THENA  Auto)  THEN  ((Assert  oal\_grp(s;g)  \mmember{}  OMon)  THENA  Auto))

---

Home Index