---

Step * 4 of Lemma pes-axioms


1. the_es : EO@i'
⊢ ∀e:E. (↑first(e) ⇐⇒ ∀e':E. (¬(e' <loc e)))
BY
{ (RWO "assert-es-first" 0 THEN Auto) }

1
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)

2
1. the_es : EO@i'
2. e : E@i
3. ∀e':E. (¬(e' <loc e))@i
4. e' : E
5. loc(e') = loc(e) ∈ Id
⊢ ¬(e' < e)

---

Latex:



1.  the$_{es}$  :  EO@i'
\mvdash{}  \mforall{}e:E.  (\muparrow{}first(e)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}e':E.  (\mneg{}(e'  <loc  e)))


By

(RWO  "assert-es-first"  0  THEN  Auto)

---

Home Index