Step * 7 of Lemma pes-axioms


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


Latex:


Latex:

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


By


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




Home Index