---

Step * 4 1 of Lemma pes-axioms


1. the_es : EO@i'
2. e : E@i
3. ∀[e':E]. ¬(e' < e) supposing loc(e') = loc(e) ∈ Id@i
4. e' : E@i
⊢ ¬(e' <loc e)
BY
{ ((D 0 THENA Auto) THEN InstHyp [⌈e'⌉] 3⋅ THEN Auto) }

---

Latex:



1.  the$_{es}$  :  EO@i'
2.  e  :  E@i
3.  \mforall{}[e':E].  \mneg{}(e'  <  e)  supposing  loc(e')  =  loc(e)@i
4.  e'  :  E@i
\mvdash{}  \mneg{}(e'  <loc  e)


By

((D  0  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  3\mcdot{}  THEN  Auto)

---

Home Index