---

Step * of Lemma es-le-before-ordered

∀es:EO. ∀e:E.  l-ordered(E;x,y.(x <loc y);≤loc(e))
BY
{ (Auto THEN D 0 THEN Auto THEN FLemma `l_before-es-le-before-iff` [-1] THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.    l-ordered(E;x,y.(x  <loc  y);\mleq{}loc(e))


By

(Auto  THEN  D  0  THEN  Auto  THEN  FLemma  `l\_before-es-le-before-iff`  [-1]  THEN  Auto)

---

Home Index