---

Step * of Lemma es-interval-iseg

∀es:EO. ∀e3,e2,e1:E.  (e1 ≤loc e2  ⇒ e1 ≤loc e3  ⇒ ([e1, e2] ≤ [e1, e3] ⇐⇒ e2 ≤loc e3 ))
BY
{ (((((D 0 THENA Auto) THEN LocLessInd) THENA Auto) THEN UnivCD) THENA Auto) }

1
1. es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀e2,e1:E.  (e1 ≤loc e2  ⇒ e1 ≤loc k  ⇒ ([e1, e2] ≤ [e1, k] ⇐⇒ e2 ≤loc k ))))@i
5. e2 : E@i
6. e1 : E@i
7. e1 ≤loc e2 @i
8. e1 ≤loc j @i
⊢ [e1, e2] ≤ [e1, j] ⇐⇒ e2 ≤loc j 

---

Latex:


\mforall{}es:EO.  \mforall{}e3,e2,e1:E.    (e1  \mleq{}loc  e2    {}\mRightarrow{}  e1  \mleq{}loc  e3    {}\mRightarrow{}  ([e1,  e2]  \mleq{}  [e1,  e3]  \mLeftarrow{}{}\mRightarrow{}  e2  \mleq{}loc  e3  ))


By

(((((D  0  THENA  Auto)  THEN  LocLessInd)  THENA  Auto)  THEN  UnivCD)  THENA  Auto)

---

Home Index