---

Step * of Lemma es-causl_transitivity2

∀es:EO. ∀x,y,z:E.  ((x < y) ⇒ y c≤ z ⇒ (x < z))
BY
{ (Auto THEN D -1) }

1
1. es : EO@i'
2. x : E@i
3. y : E@i
4. z : E@i
5. (x < y)@i
6. (y < z)@i
⊢ (x < z)

2
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)

---

Latex:


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


By

(Auto  THEN  D  -1)

---

Home Index