---

Step * of Lemma es-le-self

∀es:EO. ∀e:E.  e ≤loc e 
BY
{ (Unfold `es-le` 0 THEN Auto THEN OrRight THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.    e  \mleq{}loc  e 


By

(Unfold  `es-le`  0  THEN  Auto  THEN  OrRight  THEN  Auto)

---

Home Index