---

Step * of Lemma es-p-locl_transitivity

∀es:EO. ∀p:E ─→ (E + Top). ∀a,b,c:E.  (a p< b ⇒ b p< c ⇒ a p< c)
BY
{ ((Unfold `es-p-locl` 0 THEN Auto) THEN ExRepD) }

1
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. a : E@i
4. b : E@i
5. c : E@i
6. n1 : ℕ+@i
7. p-graph(E;p^n1) b a@i
8. n : ℕ+@i
9. p-graph(E;p^n) c b@i
⊢ ∃n:ℕ+. (p-graph(E;p^n) c a)

---

Latex:


\mforall{}es:EO.  \mforall{}p:E  {}\mrightarrow{}  (E  +  Top).  \mforall{}a,b,c:E.    (a  p<  b  {}\mRightarrow{}  b  p<  c  {}\mRightarrow{}  a  p<  c)


By

((Unfold  `es-p-locl`  0  THEN  Auto)  THEN  ExRepD)

---

Home Index