---

Step * of Lemma es-causl_transitivity

∀es:EO. ∀x,y,z:es-base-E(es).  ((x < y) ⇒ (y < z) ⇒ (x < z))
BY
{ (InstLemma `event_ordering_properties` [] THEN ParallelLast THEN SplitAndHyps THEN Trivial) }

---

Latex:


\mforall{}es:EO.  \mforall{}x,y,z:es-base-E(es).    ((x  <  y)  {}\mRightarrow{}  (y  <  z)  {}\mRightarrow{}  (x  <  z))


By

(InstLemma  `event\_ordering\_properties`  []  THEN  ParallelLast  THEN  SplitAndHyps  THEN  Trivial)

---

Home Index