---

Step * of Lemma es-first-implies

∀[the_es:EO]. ∀[j,e:E].  ¬(e <loc j) supposing ↑first(j)
BY
{ (Use_ES_Axioms THEN Auto THEN BHyp 5 THEN Auto) }

---

Latex:


\mforall{}[the$_{es}$:EO].  \mforall{}[j,e:E].    \mneg{}(e  <loc  j)  supposing  \muparrow{}first(j)


By

(Use\_ES\_Axioms  THEN  Auto  THEN  BHyp  5  THEN  Auto)

---

Home Index