---

Step * of Lemma alle-between1-trivial

∀es:EO. ∀e:E. ∀P:Top.  ∀e∈[e,e).P[e]
BY
{ (Auto
   THEN UnfoldTopAb 0
   THEN Auto
   THEN ((InstLemma `es-locl-antireflexive` [⌈es⌉; ⌈e⌉])⋅ THENA Auto)
   THEN D -1
   THEN (Using [`b',⌈e@0⌉] (BLemma `es-le-trans2`))⋅
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.  \mforall{}P:Top.    \mforall{}e\mmember{}[e,e).P[e]


By

(Auto
  THEN  UnfoldTopAb  0
  THEN  Auto
  THEN  ((InstLemma  `es-locl-antireflexive`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (Using  [`b',\mkleeneopen{}e@0\mkleeneclose{}]  (BLemma  `es-le-trans2`))\mcdot{}
  THEN  Auto)

---

Home Index