---

Step * of Lemma es-le-linorder

∀es:EO. ∀i:Id.  Linorder({e:E| loc(e) = i ∈ Id} ;a,b.a ≤loc b )
BY
{ (RepUR ``linorder order connex refl trans anti_sym`` 0 THEN Auto) }

1
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} 

2
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 

---

Latex:


\mforall{}es:EO.  \mforall{}i:Id.    Linorder(\{e:E|  loc(e)  =  i\}  ;a,b.a  \mleq{}loc  b  )


By

(RepUR  ``linorder  order  connex  refl  trans  anti\_sym``  0  THEN  Auto)

---

Home Index