---

Step * of Lemma eo-forward-causle-implies

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e:E]. ∀[e1,e2:E].  (e1 c≤ e2 ⇒ e1 c≤ e2)
BY
{ (Auto THEN RWO "eo-forward-causle" (-1) THEN Auto THEN FLemma `eo-forward-E-member` [-1] THEN Auto) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e:E].  \mforall{}[e1,e2:E].    (e1  c\mleq{}  e2  {}\mRightarrow{}  e1  c\mleq{}  e2)


By

(Auto  THEN  RWO  "eo-forward-causle"  (-1)  THEN  Auto  THEN  FLemma  `eo-forward-E-member`  [-1]  THEN  Auto)

---

Home Index