---

Step * of Lemma es-knows-stable

∀[poss:EO ─→ ℙ']. ∀[R:PossibleEvent(poss) ─→ PossibleEvent(poss) ─→ ℙ'].
  (Trans(PossibleEvent(poss))(R _1 _2)
  ⇒ (∀e1,e2:PossibleEvent(poss).  (e1 ≤ e2 ⇒ (R e1 e2)))
  ⇒ (∀[P:PossibleEvent(poss) ─→ ℙ']. ∀e1,e2:PossibleEvent(poss).  (e1 ≤ e2 ⇒ K(P)@e1 ⇒ K(P)@e2)))
BY
{ (RepUR ``es-knows`` 0 THEN Auto THEN BackThruSomeHyp THEN UseTrans ⌈e2⌉⋅ THEN BackThruSomeHyp THEN Auto) }

---

Latex:


\mforall{}[poss:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[R:PossibleEvent(poss)  {}\mrightarrow{}  PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].
    (Trans(PossibleEvent(poss))(R  $_{1}$  $_{2}$)
    {}\mRightarrow{}  (\mforall{}e1,e2:PossibleEvent(poss).    (e1  \mleq{}  e2  {}\mRightarrow{}  (R  e1  e2)))
    {}\mRightarrow{}  (\mforall{}[P:PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}e1,e2:PossibleEvent(poss).    (e1  \mleq{}  e2  {}\mRightarrow{}  K(P)@e1  {}\mRightarrow{}  K(P)@e2)))


By

(RepUR  ``es-knows``  0
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  UseTrans  \mkleeneopen{}e2\mkleeneclose{}\mcdot{}
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index