---

Step * 1 of Lemma alle-between3-false


1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. ∀e:E. ((e1 <loc e) ⇒ e ≤loc e2  ⇒ False)@i
⊢ e2 ≤loc e1 
BY
{ (SupposeNot THEN (InstHyp [⌈e2⌉] (-2))⋅ THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e1  :  E@i
3.  e2  :  \{e:E|  loc(e)  =  loc(e1)\}  @i
4.  \mforall{}e:E.  ((e1  <loc  e)  {}\mRightarrow{}  e  \mleq{}loc  e2    {}\mRightarrow{}  False)@i
\mvdash{}  e2  \mleq{}loc  e1 


By

(SupposeNot  THEN  (InstHyp  [\mkleeneopen{}e2\mkleeneclose{}]  (-2))\mcdot{}  THEN  Auto)

---

Home Index