---

Step * 1 2 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
{ ((OrLeft THENA Auto) THEN BLemma `es-pred-less-base` 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.  \mneg{}(pred(e)  =  e)
\mvdash{}  (pred(e)  <  e)  \mvee{}  (pred(e)  =  e)


By

((OrLeft  THENA  Auto)  THEN  BLemma  `es-pred-less-base`  THEN  Auto)

---

Home Index