---

Step * of Lemma es-causl_weakening

∀es:EO. ∀a,b:E.  ((a <loc b) ⇒ (a < b))
BY
{ (Auto THEN (InstESAxiom ⌈es⌉ [] 10)⋅ THEN (BHyp (-1)) THEN Auto) }

---

Latex:


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


By

(Auto  THEN  (InstESAxiom  \mkleeneopen{}es\mkleeneclose{}  []  10)\mcdot{}  THEN  (BHyp  (-1))  THEN  Auto)

---

Home Index