---

Step * of Lemma es-all-events_wf

∀[Info:Type]. ∀[es:EO+(Info)].  (E ∈ EClass(Top))
BY
{ (Unfolds ``es-all-events eclass`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].    (E  \mmember{}  EClass(Top))


By

---

Latex:
(Unfolds  ``es-all-events  eclass``  0  THEN  Auto)

---

Home Index