---

Step * of Lemma oal_bpos_trichot

∀s:LOSet. ∀g:OGrp. ∀rs:|oal(s;g)|.  ((↑pos(rs)) ∨ (rs = 00 ∈ |oal(s;g)|) ∨ (↑pos(--rs)))
BY
{ TACTIC:(RepeatFor 2 ((D 0 THENA Auto))
          THEN ((Assert g ∈ AbDMon BY
                       (BLemma `omon_inc` THEN Auto))
                THEN (Assert g ∈ AbDGrp BY
                            (BLemma `ocgrp_abdgrp` THEN Auto))
                )
          THEN Auto) }

1
1. s : LOSet
2. g : OGrp
3. g ∈ AbDMon
4. g ∈ AbDGrp
5. rs : |oal(s;g)|
⊢ (↑pos(rs)) ∨ (rs = 00 ∈ |oal(s;g)|) ∨ (↑pos(--rs))

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.  \mforall{}rs:|oal(s;g)|.    ((\muparrow{}pos(rs))  \mvee{}  (rs  =  00)  \mvee{}  (\muparrow{}pos(--rs)))


By

---

Latex:
TACTIC:(RepeatFor  2  ((D  0  THENA  Auto))
                THEN  ((Assert  g  \mmember{}  AbDMon  BY
                                          (BLemma  `omon\_inc`  THEN  Auto))
                            THEN  (Assert  g  \mmember{}  AbDGrp  BY
                                                    (BLemma  `ocgrp\_abdgrp`  THEN  Auto))
                            )
                THEN  Auto)

---

Home Index