---

Step * of Lemma es-causal-antireflexive

∀[the_es:EO]. ∀[e:es-base-E(the_es)].  (¬(e < e))
BY
{ (BasicUniformUnivCD Auto
   THEN (InstLemma `es-causl-wf-base` [⌜the_es⌝]⋅ THENA Auto)
   THEN D 0
   THEN Auto
   THEN (InstLemma `es-rank-wf-base` [⌜the_es⌝;⌜e⌝]⋅ THENA Auto)) }

1
1. the_es : EO
2. e : es-base-E(the_es)
3. ∀[e,e':es-base-E(the_es)].  ((e < e') ∈ ℙ)
4. (e < e)@i
5. es-rank(the_es;e) ∈ ℕ
⊢ False

---

Latex:

---

Latex:
\mforall{}[the$_{es}$:EO].  \mforall{}[e:es-base-E(the$_{es}$)].    (\mneg{}(e  <  e))


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  (InstLemma  `es-causl-wf-base`  [\mkleeneopen{}the$_{es}$\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  0
  THEN  Auto
  THEN  (InstLemma  `es-rank-wf-base`  [\mkleeneopen{}the$_{es}$\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index