---

Step * 1 of Lemma es-le-linorder


1. es : EO@i'
2. i : Id@i
3. ∀a:{e:E| loc(e) = i ∈ Id} . a ≤loc a 
4. ∀a,b,c:{e:E| loc(e) = i ∈ Id} .  (a ≤loc b  ⇒ b ≤loc c  ⇒ a ≤loc c )
5. a : {e:E| loc(e) = i ∈ Id} @i
6. b : {e:E| loc(e) = i ∈ Id} @i
7. a ≤loc b @i
8. b ≤loc a @i
⊢ a = b ∈ {e:E| loc(e) = i ∈ Id} 
BY
{ (D -1 THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  i  :  Id@i
3.  \mforall{}a:\{e:E|  loc(e)  =  i\}  .  a  \mleq{}loc  a 
4.  \mforall{}a,b,c:\{e:E|  loc(e)  =  i\}  .    (a  \mleq{}loc  b    {}\mRightarrow{}  b  \mleq{}loc  c    {}\mRightarrow{}  a  \mleq{}loc  c  )
5.  a  :  \{e:E|  loc(e)  =  i\}  @i
6.  b  :  \{e:E|  loc(e)  =  i\}  @i
7.  a  \mleq{}loc  b  @i
8.  b  \mleq{}loc  a  @i
\mvdash{}  a  =  b


By

(D  -1  THEN  Auto)

---

Home Index