---

Step * of Lemma es-le-total

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

---

Latex:


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


By

(Auto
  THEN  (Inst\_ES\_Axiom  [\mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{}]  3)\mcdot{}
  THEN  Auto
  THEN  SplitOrHyps
  THEN  ((OrLeft  THEN  Complete  (Auto))  ORELSE  (OrRight  THEN  Complete  (Auto))))

---

Home Index