---

Step * of Lemma same-loc-total2

∀es:EO. ∀e,e':E.  (e < e') ∨ (e' = e ∈ E) ∨ (e' < e) supposing loc(e) = loc(e') ∈ Id
BY
{ (InstLemma `same-loc-total` [] THEN RepeatFor 6 (ParallelLast)) }

---

Latex:


\mforall{}es:EO.  \mforall{}e,e':E.    (e  <  e')  \mvee{}  (e'  =  e)  \mvee{}  (e'  <  e)  supposing  loc(e)  =  loc(e')


By

(InstLemma  `same-loc-total`  []  THEN  RepeatFor  6  (ParallelLast))

---

Home Index