---

Step * of Lemma oal_lt_trichot

∀s:LOSet. ∀g:OGrp. ∀ps,qs:|oal(s;g)|.  ((ps << qs) ∨ (ps = qs ∈ |oal(s;g)|) ∨ (qs << ps))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN Assert ⌜(g ∈ AbDGrp) ∧ (g ∈ AbDMon)⌝⋅) }

1
.....assertion..... 
1. s : LOSet
2. g : OGrp
⊢ (g ∈ AbDGrp) ∧ (g ∈ AbDMon)

2
1. s : LOSet
2. g : OGrp
3. (g ∈ AbDGrp) ∧ (g ∈ AbDMon)
⊢ ∀ps,qs:|oal(s;g)|.  ((ps << qs) ∨ (ps = qs ∈ |oal(s;g)|) ∨ (qs << ps))

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.  \mforall{}ps,qs:|oal(s;g)|.    ((ps  <<  qs)  \mvee{}  (ps  =  qs)  \mvee{}  (qs  <<  ps))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  Assert  \mkleeneopen{}(g  \mmember{}  AbDGrp)  \mwedge{}  (g  \mmember{}  AbDMon)\mkleeneclose{}\mcdot{})

---

Home Index