---

Step * 1 1 of Lemma oal_bpos_wf

.....truecase..... 
1. s : LOSet
2. g : AbDMon
3. ps : |oal(s;g)|
4. ¬(ps = 00 ∈ |oal(s;g)|)
⊢ e <b lv(ps) ∈ 𝔹
BY
{ % Note how bpos set up so this is automatic % 
Auto }

---

Latex:

---

Latex:
.....truecase..... 
1.  s  :  LOSet
2.  g  :  AbDMon
3.  ps  :  |oal(s;g)|
4.  \mneg{}(ps  =  00)
\mvdash{}  e  <\msubb{}  lv(ps)  \mmember{}  \mBbbB{}


By

---

Latex:
\%  Note  how  bpos  set  up  so  this  is  automatic  \% 
Auto

---

Home Index