---

Step * 2 of Lemma oal_lt_trichot


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))
BY
{ ((RepD THENM RWW "assert_of_oal_blt<" 0) THENA Auto) }

1
1. s : LOSet
2. g : OGrp
3. g ∈ AbDGrp
4. g ∈ AbDMon
5. ps : |oal(s;g)|
6. qs : |oal(s;g)|
⊢ (↑(ps <<b qs)) ∨ (ps = qs ∈ |oal(s;g)|) ∨ (↑(qs <<b ps))

---

Latex:

---

Latex:

1.  s  :  LOSet
2.  g  :  OGrp
3.  (g  \mmember{}  AbDGrp)  \mwedge{}  (g  \mmember{}  AbDMon)
\mvdash{}  \mforall{}ps,qs:|oal(s;g)|.    ((ps  <<  qs)  \mvee{}  (ps  =  qs)  \mvee{}  (qs  <<  ps))


By

---

Latex:
((RepD  THENM  RWW  "assert\_of\_oal\_blt<"  0)  THENA  Auto)

---

Home Index