---

Step * of Lemma es-locl-total

∀es:EO. ∀e,e':E.  (e <loc e') ∨ (e = e' ∈ E) ∨ (e' <loc e) supposing loc(e) = loc(e') ∈ Id
BY
{ (Auto THEN (Inst_ES_Axiom [⌈e⌉; ⌈e'⌉] 3)⋅ THEN Auto) }

---

Latex:


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


By

(Auto  THEN  (Inst\_ES\_Axiom  [\mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{}]  3)\mcdot{}  THEN  Auto)

---

Home Index