---

Step * of Lemma es-locl-irreflex-test

∀[es:EO]. ∀[e2,e:E].  ¬(e = e2 ∈ E) supposing (e <loc e2)
BY
{ Auto }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e2,e:E].    \mneg{}(e  =  e2)  supposing  (e  <loc  e2)


By

Auto

---

Home Index