---

Step * of Lemma causal-weak-predecessor_wf

∀[es:EO]. ∀[p:E ─→ (E + Top)].  (causal-weak-predecessor(es;p) ∈ ℙ)
BY
{ ((Auto THEN Unfold `causal-weak-predecessor` 0) THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[p:E  {}\mrightarrow{}  (E  +  Top)].    (causal-weak-predecessor(es;p)  \mmember{}  \mBbbP{})


By

((Auto  THEN  Unfold  `causal-weak-predecessor`  0)  THEN  Auto)

---

Home Index