---

Step * of Lemma K-le_reflexive

∀K:mKripkeStruct. ∀i:World.  i ≤ i
BY
{ (((Auto THEN RepUR ``K-le`` 0) THEN DKripke 1) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}K:mKripkeStruct.  \mforall{}i:World.    i  \mleq{}  i


By

---

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

---

Home Index