---

Step * of Lemma es-causal-antisymmetric

∀[es:EO]. ∀[e,e':E].  ¬(e' < e) supposing (e < e')
BY
{ (Auto THEN D 0 THEN Auto THEN ((InstLemma `es-causal-antireflexive` [⌈es⌉; ⌈e⌉])⋅ THENA Auto)) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    \mneg{}(e'  <  e)  supposing  (e  <  e')


By

(Auto  THEN  D  0  THEN  Auto  THEN  ((InstLemma  `es-causal-antireflexive`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{}])\mcdot{}  THENA  Auto))

---

Home Index