---

Step * of Lemma es-p-le_transitivity

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

1
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. a : E@i
4. b : E@i
5. c : E@i
6. a p< b@i
7. b p< c@i
⊢ a p< c ∨ (a = c ∈ E)

2
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. a : E@i
4. b : E@i
5. c : E@i
6. a = b ∈ E@i
7. b p< c@i
⊢ a p< c ∨ (a = c ∈ E)

3
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. a : E@i
4. b : E@i
5. c : E@i
6. a p< b@i
7. b = c ∈ E@i
⊢ a p< c ∨ (a = c ∈ E)

4
1. es : EO@i'
2. p : E ─→ (E + Top)@i
3. a : E@i
4. b : E@i
5. c : E@i
6. a = b ∈ E@i
7. b = c ∈ E@i
⊢ a p< c ∨ (a = c ∈ E)

---

Latex:


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


By

((Unfold  `es-p-le`  0  THEN  Auto)  THEN  SplitOrHyps)

---

Home Index