---

Step * of Lemma es-is-prior-interface

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E.  (↑e ∈b prior(X) ⇐⇒ ∃e':E. ((e' <loc e) ∧ (↑e' ∈b X)))
BY
{ (InstLemma `is-prior-interface` [] THEN ParallelLast THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  prior(X)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  ((e'  <loc  e)  \mwedge{}  (\muparrow{}e'  \mmember{}\msubb{}  X)))


By

---

Latex:
(InstLemma  `is-prior-interface`  []  THEN  ParallelLast  THEN  Auto)

---

Home Index