---

Step * of Lemma K-dom_subtype

∀[K:mKripkeStruct]. ∀[i,j:World].  Dom(i) ⊆r Dom(j) supposing i ≤ j
BY
{ ((Auto THEN DKripke 1) THEN RepUR ``K-dom`` 0 THEN RepUR ``K-le`` -1 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[K:mKripkeStruct].  \mforall{}[i,j:World].    Dom(i)  \msubseteq{}r  Dom(j)  supposing  i  \mleq{}  j


By

---

Latex:
((Auto  THEN  DKripke  1)  THEN  RepUR  ``K-dom``  0  THEN  RepUR  ``K-le``  -1  THEN  Auto)

---

Home Index