---

Step * 1 1 of Lemma es-pred_property_base


1. es : EO@i'
2. e : es-base-E(es)@i
3. ∀[e:es-base-E(es)]. (pred(e) ∈ es-base-E(es))
4. pred(e) = e ∈ es-base-E(es)
⊢ (pred(e) < e) ∨ (pred(e) = e ∈ es-base-E(es))
BY
{ ((InstLemma `es-causl-wf-base` [⌈es⌉;⌈pred(e)⌉;⌈e⌉]⋅ THENA Auto) THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  es-base-E(es)@i
3.  \mforall{}[e:es-base-E(es)].  (pred(e)  \mmember{}  es-base-E(es))
4.  pred(e)  =  e
\mvdash{}  (pred(e)  <  e)  \mvee{}  (pred(e)  =  e)


By

((InstLemma  `es-causl-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}pred(e)\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Auto)

---

Home Index