---

Step * of Lemma es-le_antisymmetry

∀[es:EO]. ∀[e,e':E].  (e = e' ∈ E) supposing (e' ≤loc e  and e ≤loc e' )
BY
{ (skip{RelRST needs this lemma to have exactly this name!} THEN (InstLemma `es-le-antisymmetric` []) THEN Trivial) }

---

Latex:


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


By

(skip\{RelRST  needs  this  lemma  to  have  exactly  this  name!\}
  THEN  (InstLemma  `es-le-antisymmetric`  [])
  THEN  Trivial)

---

Home Index