---

Step * 1 of Lemma es-closed-open-interval-sorted-by


1. [Info] : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
⊢ sorted-by(λx,y. (x <loc y);before(e2))
BY
{ ((RWO "l-ordered-is-sorted-by<" 0 THENA Auto)
   THEN UnfoldTopAb 0
   THEN Auto
   THEN FLemma `l_before-es-before` [-1]
   THEN Auto) }

---

Latex:



1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  e1  :  E@i
4.  e2  :  E@i
\mvdash{}  sorted-by(\mlambda{}x,y.  (x  <loc  y);before(e2))


By

((RWO  "l-ordered-is-sorted-by<"  0  THENA  Auto)
  THEN  UnfoldTopAb  0
  THEN  Auto
  THEN  FLemma  `l\_before-es-before`  [-1]
  THEN  Auto)

---

Home Index