---

Step * of Lemma es-knows-trans

∀[poss:EO ⟶ ℙ']. ∀[R:PossibleEvent(poss) ⟶ PossibleEvent(poss) ⟶ ℙ']. ∀[P,Q:PossibleEvent(poss) ⟶ ℙ'].
  ((∀e:PossibleEvent(poss). ((P e) ⇒ (Q e))) ⇒ (∀e:PossibleEvent(poss). (K(P)@e ⇒ K(Q)@e)))
BY
{ (RepUR ``es-knows`` 0 THEN Auto THEN BackThruSomeHyp THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[poss:EO  {}\mrightarrow{}  \mBbbP{}'].  \mforall{}[R:PossibleEvent(poss)  {}\mrightarrow{}  PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].
\mforall{}[P,Q:PossibleEvent(poss)  {}\mrightarrow{}  \mBbbP{}'].
    ((\mforall{}e:PossibleEvent(poss).  ((P  e)  {}\mRightarrow{}  (Q  e)))  {}\mRightarrow{}  (\mforall{}e:PossibleEvent(poss).  (K(P)@e  {}\mRightarrow{}  K(Q)@e)))


By

---

Latex:
(RepUR  ``es-knows``  0  THEN  Auto  THEN  BackThruSomeHyp  THEN  Auto)

---

Home Index