---

Step * of Lemma es-locl_transitivity

∀es:EO. ∀a,b,c:E.  ((a <loc b) ⇒ (b <loc c) ⇒ (a <loc c))
BY
{ (Auto THEN ((InstLemma `es-locl-trans` [⌈es⌉])⋅ THENA Auto) THEN UseTrans ⌈b⌉⋅ THEN Auto) }

---

Latex:


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


By

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

---

Home Index