---

Step * of Lemma poss-le_wf

∀[poss:EO ⟶ ℙ']. ∀[e1,e2:PossibleEvent(poss)].  (e1 ≤ e2 ∈ ℙ')
BY
{ (RepUR ``poss-le possible-event`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[poss:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[e1,e2:PossibleEvent(poss)].    (e1  \mleq{}  e2  \mmember{}  \mBbbP{}')


By

---

Latex:
(RepUR  ``poss-le  possible-event``  0  THEN  Auto)

---

Home Index