---

Step * 1 1 of Lemma oset_of_ocmon_wf


1. g : OMon
2. Assoc(|g|;*)
3. Ident(|g|;*;e)
4. Comm(|g|;*)
5. UniformlyRefl(|g|;x,y.↑(x ≤b y))
6. UniformlyTrans(|g|;x,y.↑(x ≤b y))
7. UniformlyAntiSym(|g|;x,y.↑(x ≤b y))
8. Connex(|g|;x,y.↑(x ≤b y))
9. ∀[x,y:|g|].  ↑(x ≤b y) supposing ↑(x ≤b y)
10. IsEqFun(|g|;=b)
⊢ UniformPreorder(|g|;a,b.↑(a ≤b b))
BY
{ ((D 0) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  OMon
2.  Assoc(|g|;*)
3.  Ident(|g|;*;e)
4.  Comm(|g|;*)
5.  UniformlyRefl(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
6.  UniformlyTrans(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
7.  UniformlyAntiSym(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
8.  Connex(|g|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y))
9.  \mforall{}[x,y:|g|].    \muparrow{}(x  \mleq{}\msubb{}  y)  supposing  \muparrow{}(x  \mleq{}\msubb{}  y)
10.  IsEqFun(|g|;=\msubb{})
\mvdash{}  UniformPreorder(|g|;a,b.\muparrow{}(a  \mleq{}\msubb{}  b))


By

---

Latex:
((D  0)  THEN  Auto)

---

Home Index