---

Step * 7 of Lemma pes-axioms


1. the_es : EO@i'
⊢ SWellFounded((e < e'))
BY
{ (BLemma `es-causl-swellfnd` ⋅ THENA Auto) }

---

Latex:



1.  the$_{es}$  :  EO@i'
\mvdash{}  SWellFounded((e  <  e'))


By

(BLemma  `es-causl-swellfnd`  \mcdot{}  THENA  Auto)

---

Home Index