---

Step * of Lemma es-locl-not-le

∀es:EO. ∀e,e':E.  (e <loc e') ⇐⇒ ¬e' ≤loc e  supposing loc(e) = loc(e') ∈ Id
BY
{ Auto }

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':E.    (e  <loc  e')  \mLeftarrow{}{}\mRightarrow{}  \mneg{}e'  \mleq{}loc  e    supposing  loc(e)  =  loc(e')


By

Auto

---

Home Index