---

Step * 1 of Lemma es-locl-antireflexive


1. the_es : EO
⊢ ∀e:E. (¬(e <loc e))
BY
{ ((LocLessInd THENA Auto) THEN (D 0 THENA Auto) THEN FHyp (-2) [-1] THEN Auto) }

---

Latex:



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


By

((LocLessInd  THENA  Auto)  THEN  (D  0  THENA  Auto)  THEN  FHyp  (-2)  [-1]  THEN  Auto)

---

Home Index