---

Step * of Lemma es-locl-trichotomy

∀the_es:EO. ∀e,e':E.  (loc(e) = loc(e') ∈ Id ⇐⇒ (e <loc e') ∨ (e = e' ∈ E) ∨ (e' <loc e))
BY
{ (InstLemma `pes-axioms` [] THEN ParallelLast THEN SplitAndHyps THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}the$_{es}$:EO.  \mforall{}e,e':E.    (loc(e)  =  loc(e')  \mLeftarrow{}{}\mRightarrow{}  (e  <loc  e')  \mvee{}  (e  =  e')  \mvee{}  (e'  <lo\000Cc  e))


By

---

Latex:
(InstLemma  `pes-axioms`  []  THEN  ParallelLast  THEN  SplitAndHyps  THEN  Trivial)

---

Home Index