---

Step * 2 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,b:{e:E| loc(e) = i ∈ Id} .  (a ≤loc b  ⇒ b ≤loc a  ⇒ (a = b ∈ {e:E| loc(e) = i ∈ Id} ))
6. a : {e:E| loc(e) = i ∈ Id} @i
7. b : {e:E| loc(e) = i ∈ Id} @i
⊢ a ≤loc b  ∨ b ≤loc a 
BY
{ (BLemma `es-le-total`  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.  \mforall{}a,b:\{e:E|  loc(e)  =  i\}  .    (a  \mleq{}loc  b    {}\mRightarrow{}  b  \mleq{}loc  a    {}\mRightarrow{}  (a  =  b))
6.  a  :  \{e:E|  loc(e)  =  i\}  @i
7.  b  :  \{e:E|  loc(e)  =  i\}  @i
\mvdash{}  a  \mleq{}loc  b    \mvee{}  b  \mleq{}loc  a 


By

(BLemma  `es-le-total`    THEN  Auto)\mcdot{}

---

Home Index