---

Step * of Lemma ses-flow-has

∀s:SES. ∀es:EO+(Info). ∀e1,e2:E. ∀a:Atom1.  (ses-flow(s;es;a;e1;e2) ⇒ (e2 has a))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN BLemma `ses-flow-implies` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s:SES.  \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.  \mforall{}a:Atom1.    (ses-flow(s;es;a;e1;e2)  {}\mRightarrow{}  (e2  has  a))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  BLemma  `ses-flow-implies`  THEN  Auto)

---

Home Index