---

Step * of Lemma pe-e_wf

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

---

Latex:


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


By

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

---

Home Index