---

Step * of Lemma es-locl-antireflexive

∀[the_es:EO]. ∀[e:E].  (¬(e <loc e))
BY
{ (Auto THEN MoveToConcl (-1)) }

1
1. the_es : EO
⊢ ∀e:E. (¬(e <loc e))

---

Latex:


\mforall{}[the$_{es}$:EO].  \mforall{}[e:E].    (\mneg{}(e  <loc  e))


By

(Auto  THEN  MoveToConcl  (-1))

---

Home Index