---

Step * of Lemma es-le-linorder-interface

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀j:Id.  Linorder({e':E(X)| loc(e') = j ∈ Id} ;a,b.a ≤loc b )
BY
{ Auto }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. j : Id@i
⊢ Linorder({e':E(X)| loc(e') = j ∈ Id} ;a,b.a ≤loc b )

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}j:Id.    Linorder(\{e':E(X)|  loc(e')  =  j\}  ;a,b.a  \mleq{}loc  b  )


By

---

Latex:
Auto

---

Home Index