---

Step * of Lemma ses-sign_wf

∀[s:SES]. (Sign ∈ EClass(SecurityData × Id × Atom1))
BY
{ (Unfolds ``security-event-structure ses-info`` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[s:SES].  (Sign  \mmember{}  EClass(SecurityData  \mtimes{}  Id  \mtimes{}  Atom1))


By

---

Latex:
(Unfolds  ``security-event-structure  ses-info``  0  THEN  ProveWfLemma)

---

Home Index