---

Step * of Lemma es-le-antisymmetric

∀[es:EO]. ∀[e,e':E].  (e = e' ∈ E) supposing (e' ≤loc e  and e ≤loc e' )
BY
{ (Auto
   THEN AssertBY ⌜(e <loc e') ∨ (e = e' ∈ E) ∨ (e' <loc e)⌝
        (((InstESAxiom ⌜es⌝ [⌜e⌝; ⌜e'⌝] 3)⋅ THENA Auto) THEN (BHyp (-1)) THEN Auto)⋅
   THEN SplitOrHyps
   THEN Auto
   THEN (InstLemma `es-le-not-locl` [⌜es⌝; ⌜e⌝; ⌜e'⌝])⋅
   THEN Auto
   THEN (InstLemma `es-le-not-locl` [⌜es⌝; ⌜e'⌝; ⌜e⌝])⋅
   THEN Auto
   THEN ThinTrivial
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[es:EO].  \mforall{}[e,e':E].    (e  =  e')  supposing  (e'  \mleq{}loc  e    and  e  \mleq{}loc  e'  )


By

---

Latex:
(Auto
  THEN  AssertBY  \mkleeneopen{}(e  <loc  e')  \mvee{}  (e  =  e')  \mvee{}  (e'  <loc  e)\mkleeneclose{}
            (((InstESAxiom  \mkleeneopen{}es\mkleeneclose{}  [\mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{}]  3)\mcdot{}  THENA  Auto)  THEN  (BHyp  (-1))  THEN  Auto)\mcdot{}
  THEN  SplitOrHyps
  THEN  Auto
  THEN  (InstLemma  `es-le-not-locl`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  (InstLemma  `es-le-not-locl`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e'\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  ThinTrivial
  THEN  Auto)

---

Home Index