---

Step * of Lemma es-pred-locl

∀the_es:EO. ∀j:E.  (pred(j) <loc j) supposing ¬↑first(j)
BY
{ (Use_ES_Axioms THEN Auto THEN (InstHyp [⌜j⌝] 6)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}the$_{es}$:EO.  \mforall{}j:E.    (pred(j)  <loc  j)  supposing  \mneg{}\muparrow{}first(j)


By

---

Latex:
(Use\_ES\_Axioms  THEN  Auto  THEN  (InstHyp  [\mkleeneopen{}j\mkleeneclose{}]  6)\mcdot{}  THEN  Auto)

---

Home Index