---

Step * of Lemma es-causl_transitivity1

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

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 ∈ E@i
6. (y < z)@i
⊢ (x < z)

---

Latex:


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


By

(Auto  THEN  D  -2)

---

Home Index