---

Step * of Lemma K-le_wf

∀[K:mKripkeStruct]. ∀[i,j:World].  (i ≤ j ∈ ℙ)
BY
{ (Intros THEN Unhide THEN DKripke 1 THEN All (RepUR ``K-world K-le``) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[K:mKripkeStruct].  \mforall{}[i,j:World].    (i  \mleq{}  j  \mmember{}  \mBbbP{})


By

---

Latex:
(Intros  THEN  Unhide  THEN  DKripke  1  THEN  All  (RepUR  ``K-world  K-le``)  THEN  Auto)

---

Home Index