---

Step * of Lemma pe-es_wf

∀[p:EO ⟶ ℙ']. ∀[e:PossibleEvent(p)].  (pe-es(e) ∈ EO)
BY
{ (Unfolds ``pe-es possible-event`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[e:PossibleEvent(p)].    (pe-es(e)  \mmember{}  EO)


By

---

Latex:
(Unfolds  ``pe-es  possible-event``  0  THEN  Auto)

---

Home Index