---

Step * of Lemma no-classrel-in-interval-trivial

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E].  (no X between e and e)
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN Assert ⌈(e <loc e)⌉⋅
   THEN Auto
   THEN InstLemma `es-locl-antireflexive` [⌈es⌉;⌈e⌉]⋅
   THEN Auto) }

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].    (no  X  between  e  and  e)


By

(Auto
  THEN  D  0
  THEN  Auto
  THEN  Assert  \mkleeneopen{}(e  <loc  e)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  InstLemma  `es-locl-antireflexive`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index