---

Step * of Lemma first-event_wf

∀[es:EO]. ∀[e:E].  (first-event{i:l}(es;e) ∈ E)
BY
{ (Unfold `first-event` 0 THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e:E].    (first-event\{i:l\}(es;e)  \mmember{}  E)


By

(Unfold  `first-event`  0  THEN  Auto)

---

Home Index