---

Step * of Lemma es-le_transitivity

∀es:EO. ∀a,b,c:E.  (a ≤loc b  ⇒ b ≤loc c  ⇒ a ≤loc c )
BY
{ (Auto THEN ((InstLemma `es-le-trans` [⌜es⌝])⋅ THENA Auto) THEN UseTrans ⌜b⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}a,b,c:E.    (a  \mleq{}loc  b    {}\mRightarrow{}  b  \mleq{}loc  c    {}\mRightarrow{}  a  \mleq{}loc  c  )


By

---

Latex:
(Auto  THEN  ((InstLemma  `es-le-trans`  [\mkleeneopen{}es\mkleeneclose{}])\mcdot{}  THENA  Auto)  THEN  UseTrans  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index