Step
*
of Lemma
es-p-locl_transitivity1
∀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
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 p< b@i
7. b = c ∈ E@i
⊢ a p< c
Latex:
\mforall{}es:EO. \mforall{}p:E {}\mrightarrow{} (E + Top). \mforall{}a,b,c:E. (a p< b {}\mRightarrow{} b p\mleq{} c {}\mRightarrow{} a p< c)
By
((Unfold `es-p-le` 0 THEN Auto) THEN SplitOrHyps)
Home
Index