---

Step * of Lemma es-first-exists

∀es:EO. ∀e':E.  ∃e:E. ((↑first(e)) ∧ e ≤loc e' )
BY
{ ((D 0 THENA Auto) THEN LocLessInd THEN Auto) }

1
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∃e:E. ((↑first(e)) ∧ e ≤loc k )))@i
⊢ ∃e:E. ((↑first(e)) ∧ e ≤loc j )

---

Latex:


\mforall{}es:EO.  \mforall{}e':E.    \mexists{}e:E.  ((\muparrow{}first(e))  \mwedge{}  e  \mleq{}loc  e'  )


By

((D  0  THENA  Auto)  THEN  LocLessInd  THEN  Auto)

---

Home Index