---

Step * 2 of Lemma es-causl_transitivity2


1. es : EO@i'
2. x : E@i
3. y : E@i
4. z : E@i
5. (x < y)@i
6. y = z ∈ E@i
⊢ (x < z)
BY
{ (RevHypSubst' -1 0 THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  x  :  E@i
3.  y  :  E@i
4.  z  :  E@i
5.  (x  <  y)@i
6.  y  =  z@i
\mvdash{}  (x  <  z)


By

(RevHypSubst'  -1  0  THEN  Auto)

---

Home Index