---

Step * of Lemma possible-event_wf

∀[poss:EO ─→ ℙ']. (PossibleEvent(poss) ∈ ℙ')
BY
{ (Unfold `possible-event` 0 THEN Auto) }

---

Latex:


\mforall{}[poss:EO  {}\mrightarrow{}  \mBbbP{}'].  (PossibleEvent(poss)  \mmember{}  \mBbbP{}')


By

(Unfold  `possible-event`  0  THEN  Auto)

---

Home Index