---

Step * of Lemma p-open-member_wf

∀[p:FinProbSpace]. ∀[C:p-open(p)]. ∀[s:ℕ ─→ Outcome].  (s ∈ C ∈ ℙ)
BY
{ (Unfolds ``p-open-member p-open`` 0 THEN Auto) }

---

Latex:


\mforall{}[p:FinProbSpace].  \mforall{}[C:p-open(p)].  \mforall{}[s:\mBbbN{}  {}\mrightarrow{}  Outcome].    (s  \mmember{}  C  \mmember{}  \mBbbP{})


By

(Unfolds  ``p-open-member  p-open``  0  THEN  Auto)

---

Home Index