---

Step * of Lemma oal_bpos_wf

∀s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  (pos(ps) ∈ 𝔹)
BY
{ ((RepD THENM Unfold `oal_bpos` 0) THENA Auto) }

1
1. s : LOSet
2. g : AbDMon
3. ps : |oal(s;g)|
⊢ (¬bnull(ps)) ∧b (e <b lv(ps)) ∈ 𝔹

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:AbDMon.  \mforall{}ps:|oal(s;g)|.    (pos(ps)  \mmember{}  \mBbbB{})


By

---

Latex:
((RepD  THENM  Unfold  `oal\_bpos`  0)  THENA  Auto)

---

Home Index