---

Step * of Lemma oset_of_ocmon_wf

∀[g:OMon]. (g↓oset ∈ LOSet)
BY
{ ((D 0 THENM AddAllProperties (-1)) THENA Auto) }

1
1. g : OMon
2. IsMonoid(|g|;*;e)
3. Comm(|g|;*)
4. UniformLinorder(|g|;x,y.↑(x ≤b y)) ∧ IsEqFun(|g|;=b)
⊢ g↓oset ∈ LOSet

---

Latex:

---

Latex:
\mforall{}[g:OMon].  (g\mdownarrow{}oset  \mmember{}  LOSet)


By

---

Latex:
((D  0  THENM  AddAllProperties  (-1))  THENA  Auto)

---

Home Index