---

Step * of Lemma es-causl-trans3

∀es:EO. ∀a,b,c:E.  ((a < b) ⇒ b c≤ c ⇒ (a < c))
BY
{ ((Auto THEN D -1) THENL [((InstESAxiom ⌜es⌝ [] 6)⋅ THEN UseTrans ⌜b⌝⋅ THEN Auto); (RevHypSubst' -1 0 THEN Auto)]) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  D  -1)
  THENL  [((InstESAxiom  \mkleeneopen{}es\mkleeneclose{}  []  6)\mcdot{}  THEN  UseTrans  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  Auto);  (RevHypSubst'  -1  0  THEN  Auto)]
)

---

Home Index